Abstracting Syntax: Coq Code

These are the Coq sources for the paper "Abstracting Syntax" by Brian Aydemir, Stephanie Weirich, and Steve Zdancewic. From this page, you can view HTML versions of each of the files in our developments. We provide this mainly to make it easy to browse the developments at a high level. For more details about our particular formulation of locally nameless representation, see the paper Engineering Formal Metatheory by Aydemir, Chargéraud, Pierce, Pollack, and Weirich.

Metatheory library

This is our library for programming language metatheory that we developed as part of previous work.

All the developments also share a common "tag" type.

Common

Locally nameless reference implementation

Collapsed implementation

Tagged implementation

Collapsed implementation, including collapsed binding

HOAS implementation with untyped lambda calculus

Library code:

Lib_Untyped_Lambda

Fsub development:

HOAS implementation with typed lambda calculus

Library code:

Lib_Typed_Lambda

Fsub development:

Adequacy proofs

The proof scripts for the files below here are somewhat ugly and take a significant amount of time to process. However, the developments themselves, should be reasonably readable; the scripts are elided from the HTML documentation. Note that the definition of senv_bijection is actually interesting in HOAS_Typed. For the other developments, the definition is trivial and included mainly to make comparisons to HOAS_Typed a bit easier.