BindingRepresentation
Paper programming languages proofs often follow the Barendregt variable convention. This says that alpha equivalent terms (e.g. \x.x z and \y.y z are implicitly identified. While the convention is convenient on paper, it does not translate automatically to a formal setting. The following papers (and tutorial) discuss approaches to formalizing languages with binding.
- Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich. Engineering Formal Metatheory. This paper argues for locally nameless terms and cofinitely quantified judgments. The approach appears practical for general research purposes.
- Using Proof Assistants for Programming Language Research. A tutorial based on the locally nameless/cofinite approach.
- Brian Aydemir, Stephanie Weirich, and Steve Zdancewic. Abstracting Syntax (Draft). This paper suggests several other shemes including a higher order abstract syntax encoding in Coq. The techniques mostly refine those described above.
- Brian Aydemir, Aaron Bohannon, and Stephanie Weirich. Nominal Reasoning Techniques in Coq (Extended Abstract). This paper illustrates defining expressions in terms of an (uninstantiated) nominal-logic style signature.
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.