Redundancies in Dependently Typed Lambda Calculi and Their Relevance to Proof Search

Dependently typed -calculi such as the Logical Framework (LF) are capable of representing relationships between terms through types. By exploiting the "formulas-as-types" notion, such calculi can also encode the correspondence between formulas and their proofs in typing judgments. As such, these calculi provide a natural yet powerful means for specifying varied formal systems. Such specifications can be transformed into a more direct form that uses predicate formulas over simply typed -terms and that thereby provides the basis for their animation using conventional logic programming techniques. However, a naive use of this idea is fraught with inefficiencies arising from the fact that dependently typed expressions typically contain much redundant typing information. We investigate syntactic criteria for recognizing and, hence, eliminating such redundancies. In particular, we identify a property of bound variables in LF types called rigidity and formally show that checking tha...

• Type: Journal
• Year: 2010
• Where: CORR
• Authors: Zachary Snow, David Baelde, Gopalan Nadathur
• Keywords: Conventional Logic Programming, CORR 2010, Education, Logical Framework, Typing