# 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.

## Locally nameless reference implementation

## Collapsed implementation

## Tagged implementation

## Collapsed implementation, including collapsed binding

## HOAS implementation with untyped lambda calculus

Library code:

Fsub development:

## HOAS implementation with typed lambda calculus

Library code:

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.