A Logical Framework with Explicit Conversions

The type theory P corresponds to the logical framework LF. In this paper we present H, a variant of P where convertibility is not implemented by means of the customary conversion rule, but instead type conversions are made explicit in the terms. This means that the time to type check a H term is proportional to the size of the term itself. We define an erasure map from H to P, and show that through this map the type theory H corresponds exactly to P: any H judgment will be erased to a P judgment, and conversely each P judgment can be lifted to a H judgment. We also show a version of subject reduction: if two H terms are provably convertible then their types are also provably convertible.

• Type: Journal
• Year: 2008
• Where: ENTCS
• Authors: Herman Geuvers, Freek Wiedijk
• Keywords: Customary Conversion Rule, ENTCS 2008, Logical Framework Lf, Type Theory