2 papers
cs.LO2010
Redundancies in Dependently Typed Lambda Calculi and Their Relevance to Proof Search
Zachary Snow, David Baelde, Gopalan Nadathur
Dependently typed lambda calculi such as the Logical Framework (LF) are capable of representing relationships between terms through types. By exploiting the "formulas-as-types" not…
cs.LO2010
A Meta-Programming Approach to Realizing Dependently Typed Logic Programming
Zachary Snow, David Baelde, Gopalan Nadathur
Dependently typed lambda calculi such as the Logical Framework (LF) can encode relationships between terms in types and can naturally capture correspondences between formulas and t…