International Conference on Principles and Practice of Declarative
September 29 - October 1, 1999
Carnegie Mellon University
School of Computer Science
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.