root edited this page Oct 11, 2017 · 5 revisions

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.
Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.