A generic approach to proofs about substitution

Abhishek Anand, Vincent Rahli

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
Original languageEnglish
Title of host publicationProceedings of LFMTP '14 Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, Vienna, Austria, July 17, 2014
PublisherAssociation for Computing Machinery (ACM)
ISBN (Print)978-1-4503-2817-3
DOIs
Publication statusPublished - 17 Jul 2014
Event2014 International workshop on logical frameworks and meta-languages: theory and practice - Vienna, Austria
Duration: 17 Jul 201417 Jul 2014
https://dl.acm.org/citation.cfm?id=2631172&picked=prox

Conference

Conference2014 International workshop on logical frameworks and meta-languages
Abbreviated titleLFMTP '14
Country/TerritoryAustria
CityVienna
Period17/07/1417/07/14
Internet address

Fingerprint

Dive into the research topics of 'A generic approach to proofs about substitution'. Together they form a unique fingerprint.

Cite this