Sciweavers

Share
CORR
2010
Springer

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

8 years 3 months ago
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...
Zachary Snow, David Baelde, Gopalan Nadathur
Added 09 Dec 2010
Updated 09 Dec 2010
Type Journal
Year 2010
Where CORR
Authors Zachary Snow, David Baelde, Gopalan Nadathur
Comments (0)
books