Abstract
It is well known that reasoning about substitution is a huge “distraction" that inevitably gets in the way of formalizing interesting properties of languages with variable bindings. Most formalizations have their own separate definitions of terms and substitution, and properties about it. However there is a great deal of uniformity in the way substitution works and the reasons why its properties hold. We expose this uniformity by defining terms, substitution and α-equality generically in Coq by parametrizing them over a Context Free Grammar annotated with Variable binding information (CFGV).
We also provide proofs of many properties about the above definitions (enough to formalize the PER semantics of Nuprl in Coq). Unlike many other tools which generate a custom definition of substitution for each input, all instantiations of our term model share the same substitution function. The proofs about this function have been accepted by Coq's typechecker once and for all.
We also provide proofs of many properties about the above definitions (enough to formalize the PER semantics of Nuprl in Coq). Unlike many other tools which generate a custom definition of substitution for each input, all instantiations of our term model share the same substitution function. The proofs about this function have been accepted by Coq's typechecker once and for all.
Original language | English |
---|---|
Title of host publication | Proceedings of LFMTP '14 Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, Vienna, Austria, July 17, 2014 |
Publisher | Association for Computing Machinery (ACM) |
ISBN (Print) | 978-1-4503-2817-3 |
DOIs | |
Publication status | Published - 17 Jul 2014 |
Event | 2014 International workshop on logical frameworks and meta-languages: theory and practice - Vienna, Austria Duration: 17 Jul 2014 → 17 Jul 2014 https://dl.acm.org/citation.cfm?id=2631172&picked=prox |
Conference
Conference | 2014 International workshop on logical frameworks and meta-languages |
---|---|
Abbreviated title | LFMTP '14 |
Country/Territory | Austria |
City | Vienna |
Period | 17/07/14 → 17/07/14 |
Internet address |