International Conference on Principles and Practice of Declarative Programming (PPDP'99)
Paris, France
September 29 - October 1, 1999

Frank Pfenning

Carnegie Mellon University
School of Computer Science
fp@cs

Logical frameworks have been designed as meta-languages in which deductive systems can be specified naturally and concisely. By providing direct support for common concepts of logics and programming languages, framework implementations such as Isabelle allow the rapid construction of theorem proving environments for specific logics. Logical frameworks have found significant applications in a variety of areas, including program and protocol verification and safe execution of mobile code.

Recently, researchers have exploited the directness of encodings of deductive systems in logical frameworks to reason not only within but habout logics. At the core of these efforts lies the design and implementation of meta-logical frameworks - languages in which properties of logical systems can be expressed and proven.

In this tutorial talk we first provide a brief introduction to the central techniques of logical frameworks. We then analyze the requirements for meta-logical frameworks and sketch and compare three different approaches: inductive definitions [Basin and Constable 93], definitional reflection [McDowell and Miller 97], and dependent pattern matching and recursion [Schürmann and Pfenning 98]. The last appears to be most amenable to automation and we discuss its design and implementation in the Twelf system in more detail. Recent successful experiments with this implementation include automatic proofs of cut-elimination for full first-order intuitionistic logic, the diamond property for parallel reduction in the untyped lambda-calculus, and the soundness and completeness of uniform derivations for hereditary Harrop formulas.

1. David A. Basin and Robert L. Constable. Metalogical frameworks. In G. Huet and G. Plotkin, editors, Logical Environments, pages 1-29. Cambridge University Press, 1993.

2. Raymond McDowell and Dale Miller. A logic for reasoning with higher-order abstract syntax: An extended abstract. In Glynn Winskel, editor, Proceedings of the Twelfth Annual Symposium on Logic in Computer Science, pages 434-445, Warsaw, Poland, June 1997.

3. Carsten Schürmann and Frank Pfenning. Automated theorem proving in a simple meta-logic for LF. In Claude Kirchner and Hélène Kirchner, editors, Proceedings of the 15th International Conference on Automated Deduction (CADE-15), pages 286-300, Lindau, Germany, July 1998. Springer-Verlag LNCS 1421.