TY - GEN
T1 - Towards extracting explicit proofs from totality checking in twelf
AU - Wang, Yuting
AU - Nadathur, Gopalan
PY - 2013
Y1 - 2013
N2 - The Edinburgh Logical Framework (LF) is a dependently type λ-calculus that can be used to encode formal systems. The versatility of LF allows specifications to be constructed also about the encoded systems. The Twelf system exploits the correspondence between formulas and types to give specifications in LF a logic programming interpretation. By interpreting particular arguments as input and others as output, specifications can be seen as describing non-deterministic functions. We can then prove meta-theorems about the encoded systems by showing particular such functions to be total. Twelf provides tools for establishing totality. However, the resulting proofs of meta-theorems are implicit in that they do not yield a certificate that can be given to a proof checker. We begin the process here of making these proofs explicit. We treat the restricted situation in Twelf where context definitions (regular worlds), mutually recursive definitions and lemmas are not used. In this setting we describe and prove correct a translation of the steps in totality checking into an actual proof in the companion logic M2.
AB - The Edinburgh Logical Framework (LF) is a dependently type λ-calculus that can be used to encode formal systems. The versatility of LF allows specifications to be constructed also about the encoded systems. The Twelf system exploits the correspondence between formulas and types to give specifications in LF a logic programming interpretation. By interpreting particular arguments as input and others as output, specifications can be seen as describing non-deterministic functions. We can then prove meta-theorems about the encoded systems by showing particular such functions to be total. Twelf provides tools for establishing totality. However, the resulting proofs of meta-theorems are implicit in that they do not yield a certificate that can be given to a proof checker. We begin the process here of making these proofs explicit. We treat the restricted situation in Twelf where context definitions (regular worlds), mutually recursive definitions and lemmas are not used. In this setting we describe and prove correct a translation of the steps in totality checking into an actual proof in the companion logic M2.
KW - Dependently typed λ-calculi
KW - Proof certificates
KW - Specification and reasoning
KW - Totality checking
UR - http://www.scopus.com/inward/record.url?scp=84885630770&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84885630770&partnerID=8YFLogxK
U2 - 10.1145/2503887.2503893
DO - 10.1145/2503887.2503893
M3 - Conference contribution
AN - SCOPUS:84885630770
SN - 9781450323826
T3 - Proceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP
SP - 55
EP - 66
BT - LFMTP 2013 - Proceedings of the 2013 ACM SIGPLAN Workshop on Logical Frameworks and Meta-Languages
T2 - 8th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2013 - Co-located with the 18th ACM SIGPLAN International Conference on Functional Programming, ICFP 2013
Y2 - 23 September 2013 through 23 September 2013
ER -