Mechanizing metatheory in a logical framework

13 years 4 months ago

Download www.cs.cmu.edu

The LF logical framework codiﬁes 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 deﬁnes 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 veriﬁcation of proofs of metatheorems about it. The purpose of this paper is to provide an up-to-date overview of the LF λ-calculus, the LF methodology for adequate represent...

Robert Harper, Daniel R. Licata

Real-time Traffic