Hostname: page-component-586b7cd67f-g8jcs Total loading time: 0 Render date: 2024-11-24T18:17:02.807Z Has data issue: false hasContentIssue false
  • English
  • Français

Mechanizing metatheory in a logical framework

Published online by Cambridge University Press:  01 July 2007

ROBERT HARPER  and
DANIEL R. LICATA
ROBERT HARPER
Affiliation:
Carnegie Mellon University, Pittsburgh, PA 15213, USA (e-mail: rwh@cs.cmu.edu, drl@cs.cmu.edu)
DANIEL R. LICATA
Affiliation:
Carnegie Mellon University, Pittsburgh, PA 15213, USA (e-mail: rwh@cs.cmu.edu, drl@cs.cmu.edu)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

The LF logical framework codifies a methodology for representing deductive systems, such as programming languages and logics, within a dependently typed λ-calculus. In this methodology, the syntactic and deductive apparatus of a system is encoded as the canonical forms of associated LF types; an encoding is correct (adequate) if and only if it defines a compositional bijection between the apparatus of the deductive system and the associated canonical forms. Given an adequate encoding, one may establish metatheoretic properties of a deductive system by reasoning about the associated LF representation. The Twelf implementation of the LF logical framework is a convenient and powerful tool for putting this methodology into practice. Twelf supports both the representation of a deductive system and the mechanical verification of proofs of metatheorems about it. The purpose of this article is to provide an up-to-date overview of the LF λ-calculus, the LF methodology for adequate representation, and the Twelf methodology for mechanizing metatheory. We begin by defining a variant of the original LF language, called Canonical LF, in which only canonical forms (long βη-normal forms) are permitted. This variant is parameterized by a subordination relation, which enables modular reasoning about LF representations. We then give an adequate representation of a simply typed λ-calculus in Canonical LF, both to illustrate adequacy and to serve as an object of analysis. Using this representation, we formalize and verify the proofs of some metatheoretic results, including preservation, determinacy, and strengthening. Each example illustrates a significant aspect of using LF and Twelf for formalized metatheory.

Type
Article
Information
Journal of Functional Programming , Volume 17 , Issue 4-5 , July 2007 , pp. 613 - 673
Copyright
Copyright © Cambridge University Press 2007

References

Acar, U. A., Blume, M. & Donham, J. (2007) A consistent semantics of self-adjusting computation. In European Symposium on Programming. New York: Springer-Verlag.Google Scholar
Anderson, P. & Pfenning, F. (2004) Verifying uniqueness in a logical framework. In Slind, K., Bunker, A.Gopalakrishnan, G. (eds), International Conference on Theorem Proving in Higher-Order Logics. Lecture Notes in Computer Science, vol. 3223. Berlin: Springer, pp. 18–33.CrossRefGoogle Scholar
Appel, A. W. (2001) Foundational proof-carrying code. In IEEE Symposium on Logic in Computer Science. Los Alamitos, CA: IEEE Computer Society, p. 247.Google Scholar
Appel, A. W. & Felty, A. P. (2002) Dependent types ensure partial correctness of theorem provers. J. Funct. Programming 14 (1), 3–19.CrossRefGoogle Scholar
Appel, A. & Leroy, X. (2006) A list-machine benchmark for mechanized metatheory. In International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice. Electronic Notes in Theoretical Computer Science, 95–108.Google Scholar
Avron, A., Honsell, F. & Mason, I. A. (1989) An overview of the Edinburgh Logical Framework. In Current Trends in Hardware Verification, Birtwistle, G.Subrahmanyam, P. A. (eds). Elsevier, New York: Springer Verlag, pp. 323–340.Google Scholar
Aydemir, B. E., Bohannon, A., Fairbairn, M., Foster, J. N., Pierce, B. C., Sewell, P., Vytiniotis, D., Washburn, G., Weirich, S., & Zdancewic, S. (2005) Mechanized metatheory for the masses: The POPLmark challenge. In International Conference on Theorem Proving in Higher-Order Logics. New York: Springer-Verlag, pp. 50–65.CrossRefGoogle Scholar
Bertot, Y. & Castéran, P. (2004) Interactive theorem proving and program development: Coq'art: The calculus of inductive constructions. Texts in Theoretical Computer Science. New York: Springer.Google Scholar
Cervesato, I. & Pfenning, F. (2002) A linear logical framework. Inf. Comput. 179 (1), 19–75.CrossRefGoogle Scholar
Cervesato, I., Pfenning, F., Walker, D. & Watkins, K. (2002) A Concurrent Logical Framework II: Examples and Applications. Tech. rept. CMU-CS-02-102. Pittsburgh PA: Department of Computer Science, Carnegie Mellon University. Revised May 2003.Google Scholar
Constable, R. L., Allen, S. F., Bromley, H. M., Cleaveland, W. R., Cremer, J. F., Harper, R. W., Howe, D. J., Knoblock, T. B., Mendler, N. P., Panangaden, P., Sasaki, J. T. & Smith, S. F. (1986) Implementing Mathematics With the NuPRL Proof Development System. Upper Saddle River, NJ: Prentice Hall.Google Scholar
Coq Development Team. (2007) The Coq Proof Assistant Reference Manual. INRIA. Available at: http://coq.inria.fr. Accessed June, 2007.Google Scholar
Coquand, T. (1991) An algorithm for testing conversion in type theory. In Logical Frameworks, Huet, G.Plotkin, Gordon D. (eds). New York: Cambridge University Press, pp 255–279.CrossRefGoogle Scholar
Crary, K. (2003) Toward a foundational typed assembly language. ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.Pittsburgh, PA: ACM Press, pp. 198–212.CrossRefGoogle Scholar
Crary, K. & Sarkar, S. (2003) Foundational certified code in a metalogical framework. In International Conference on Automated Deduction. New York: Springer-Verlag, pp. 106–120.Google Scholar
de Bruijn, N. G. (1993) Algorithmic definition of lambda-typed lambda calculus. In Logical Environment. Huet, G.Plotkin, G. D. (eds). New York: Cambridge University Press, pp. 131–145.Google Scholar
Felty, A. (1991) Encoding dependent types in an intuitionistic logic. In Logical Frameworks, Huet, G.Plotkin, G. D. (eds). New York: Cambridge University Press, pp. 214–251.Google Scholar
Fluet, M., Morrisett, G. & Ahmed, A. (2006) Linear regions are all you need. In European Symposium on Programming. New York: Springer-Verlag, pp. 7–21.Google Scholar
Garg, D. & Pfenning, F. (2006) Non-interference in constructive authorization logic. In Computer Security Foundations Workshop, pp. 183–293.CrossRefGoogle Scholar
Geuvers, H. (1992) The Church-Rosser property for βη-reduction in typed λ-calculi. In Scedrov, A. (ed), IEEE Symposium on Logic in Computer Science. Los Alamitos, CA: IEEE Press, pp. 453–460.Google Scholar
Goguen, H. (1999) Soundness of the logical framework for its typed operational semantics. In International Conference on Typed Lambda Calculi and Applications. Lecture Notes in Computer Science, vol. 1581. New York: Springer-Verlag, pp. 177–197.CrossRefGoogle Scholar
Harper, R. & Pfenning, F. (2005) On equivalence and canonical forms in the LF type theory. ACM Trans. Comput. Logic 6, 61–101.CrossRefGoogle Scholar
Harper, R., Honsell, F. & Plotkin, G. (1993) A framework for defining logics. J. Associ. Comput. Mach. 40 (1), 143–184.CrossRefGoogle Scholar
Harrison, J. (1996) HOL Light: A tutorial introduction. In Formal Methods in Computer-Aided Design. Lecture Notes in Computer Science, vol. 1166. New York: Springer-Verlag, pp. 265–269.CrossRefGoogle Scholar
Kaufmann, M., Manolios, P.Moore, J S. (2000) Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Now part of Springer.Google Scholar
Klein, G. & Nipkow, T. (2006) A machine-checked model for a Java-like language, virtual machine and compiler. ACM Trans. Programming Lang. Sys. 28 (4), 619–695.CrossRefGoogle Scholar
Lee, D. K., Crary, K. & Harper, R. (2007) Towards a mechanized metatheory of Standard ML. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York: ACM Press, pp. 173–184.Google Scholar
Leroy, X. (2006) Formal certification of a compiler back-end, or: Programming a compiler with a proof assistant. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York: ACM Press, pp. 42–54.Google Scholar
Licata, D. R. & Harper, R. (2005) A Formulation of Dependent ML With Explicit Equality Proofs. Tech. rept. CMU-CS-05-178. Pittsburgh, PA: Department of Computer Science, Carnegie Mellon University.Google Scholar
Michaylov, S. & Pfenning, F. (1991) Natural semantics and some of its meta-theory in Elf. In International Workshop on Extensions of Logic Programming, Eriksson, L. H., Hallnäs, L.Schroeder-Heister, P. (eds). Lecture Notes in Artificial Intelligence, vol. 596. New York: Springer-Verlag, pp. 299–344.Google Scholar
Miculan, M. (1997) Encoding Logical Theories of Programs, Ph.D. thesis. Pisa, Italy: Dipartimento di Informatica, Universita di Pisa.Google Scholar
Murphy, VII T., Crary, K., Harper, R. & Pfenning, F. (2004) A symmetric modal lambda calculus for distributed computing. In Ganzinger, H. (ed). IEEE Symposium on Logic in Computer Science. Los Alamitas, CA: IEEE Press, pp. 286–295.Google Scholar
Murphy, VII T., Crary, K. & Harper, R. (2005) Distributed control flow with classical modal logic. In Computer Science Logic. Lecture Notes in Computer Science, vol. 3634. New York: Springer-Verlag, pp. 51–69.CrossRefGoogle Scholar
Nanevski, A. & Morrisett, G. (2006) Dependent type theory of stateful higher-order functions. Tech. rept. TR-24-05. Cambridge, MA: Harvard Computer Science.Google Scholar
Nanevski, A., Pfenning, F. & Pientka, B. (to appear) Contextual modal type theory. ACM Transactions on Computational Logic.Google Scholar
Nederpelt, R. P., Geuvers, J. H. & de Vrijer, R. C. (eds). (1994) Selected papers on AUTOMATH. Studies in Logic and the Foundations of Mathematics, vol. 133. Amsterdam, North-Holland: Elsevier.Google Scholar
Nipkow, T., Paulson, L. C. & Wenzel, M. (2002) Isabelle/HOL — A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283. New York: Springer-Verlag.Google Scholar
Pfenning, F. (1991) Logic programming in the LF logical framework. In Logical Frameworks, Huet, G.Plotkin, G. D. (eds). New York: Cambridge University Press, pp. 149–181.CrossRefGoogle Scholar
Pfenning, F. (1992) A Proof of the Church-Rosser Theorem and Its Representation in a Logical Framework. Tech. rept. CMU-CS-92-186. Pittsburgh, PA: Department of Computer Science, Carnegie Mellon University.CrossRefGoogle Scholar
Pfenning, F. (1994) A Structural Proof of Cut Elimination and Its Representation in A Logical Framework. Tech. rept. CMU-CS-94-218. Pittsburgh, PA:Department of Computer Science, Carnegie Mellon University.Google Scholar
Pfenning, F. (1999) Logical frameworks. In Handbook of Automated Reasoning, Robinson, A. & Voronkov, A. (eds). Elsevier Science and MIT Press.Google Scholar
Pfenning, F. & Rohwedder, E. (1992) Implementing the meta-theory of deductive systems. In International Conference on Automated Deduction. Lecture Notes in Artificial Intelligence. Kapur, D. (ed). vol. 607. Springer-Verlag, pp. 537–551.Google Scholar
Pfenning, F. & Schürmann, C. (1999) System description: Twelf — a meta-logical framework for deductive systems. In International Conference on Automated Deduction, Ganzinger, H. (ed). pp. 202–206.CrossRefGoogle Scholar
Pfenning, F. & Schürmann, C. (2002) Twelf User's Guide, Version 1.4.Google Scholar
Pientka, B. & Pfenning, F. (2000) Termination and reduction checking in the logical framework. In Workshop on Automation of Proofs by Mathematical Induction. Schürmann, C. (ed).Google Scholar
Reed, J. (2006) Hybridizing a logical framework. In International Workshop on Hybrid Logic. Electronic Notes in Theoeretical Computer Science. Amsterdam: Elsevier, pp. 135–148.Google Scholar
Rohwedder, E. & Pfenning, F. (1996) Mode and termination checking for higher-order logic programs. In European Symposium on Programming, Nielson, H. R. (ed). Lecture Notes in Computer Science, vol. 1058. Springer-Verlag, pp. 296–310.Google Scholar
Salvesen, A. (1990) The Church-Rosser theorem for LF with βη-reduction. Unpublished notes to a talk given at the First Workshop on Logical Frameworks.Google Scholar
Schürmann, C. (2000) Automating the Meta-theory of Deductive Systems, Ph.D. thesis. Pittsburgh, PA: Carnegie Mellon University.Google Scholar
Schürmann, C. & Pfenning, F. (1998) Automated theorem proving in a simple meta-logic for LF. International Conference on Automated Deduction. Kirchner, C.Kirchner, H. (eds). Lecture Notes in Computer Science, vol. 1421. New York: Springer-Verlag, pp. 286–300.CrossRefGoogle Scholar
Schürmann, C. & Pfenning, F. (2003) A coverage checking algorithm for LF. In International Conference on Theorem Proving in Higher-Order Logics. New York: Springer-Verlag, pp. 120–135.CrossRefGoogle Scholar
Schürmann, C. & Stehr, M.-O. (2005) An executable formalization of the HOL/NuPRL connection in Twelf. In International Conference on Logic for Programming Artificial Intelligence and Reasoning. New York: Springer-Verlag, pp. 150–166.Google Scholar
Schürmann, C., Yu, D. & Ni, Z. (2001) A representation of Fω in LF. Electronic Notes Theoretical Computer Sci. 58 (1), 79–96.CrossRefGoogle Scholar
Schürmann, C., Poswolsky, A. & Sarnat, J. (2005) The ∇-calculus: Functional programming with higher-order encodings. International Conference on Typed Lambda Calculi and Applications. New York: Springer-Verlag, pp. 339–353.CrossRefGoogle Scholar
Simmons, R. (2005) Twelf as a Unified Framework for Language Formalization and Implementation. Tech. rept. Princetn, NJ: Princeton University. Undergraduate Senior Thesis 18679.Google Scholar
van Daalen, D. T. (1980) The Language Theory of AUTOMATH, Ph.D. thesis. Eindhoven, Netherlands: Technical University of Eindhoven.Google Scholar
Virga, R. (1999) Higher-Order Rewriting with Dependent Types, Ph.D. thesis. Pittsburgh, PA: Carnegie Mellon University.Google Scholar
Watkins, K.Cervesato, I., Pfenning, F. & Walker, D. (2002 A Concurrent Logical Framework I: Judgments and Properties. Tech. rept. CMU-CS-02-101. Pittsburgh PA: Department of Computer Science, Carnegie Mellon University. Revised May 2003.CrossRefGoogle Scholar
Watkins, K.Cervesato, I.Pfenning, F. & Walker, D. (2004a) A concurrent logical framework: The propositional fragment. In Types for Proofs and Programs, Berardi, S., Coppo, M.Damiani, F. (eds). Lecture Notes in Computer Science, vol. 3085. New York: Springer-Verlag, pp. 355–377.CrossRefGoogle Scholar
Watkins, K., Cervesato, I., Pfenning, F. & Walker, D. (2004b) Specifying properties of concurrent computations in CLF. In International Workshop on Logical Frameworks and Meta-Languages, Schürmann, C. (ed).Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.