The Coq sources are available at our github repository . This page is a semantic index for the above collection of files. For an index of proofs mentioned in the paper, visit: LFMTPProofs

- General library code to augment Coq's standard library: universe.v UsefulTypes.v list.v AssociationList.v
- Definition of Variables GVariables.v
- Definition of CFGV CFGV.v
- Complete CFGV specification of the example language in the paper. LetrecEx.v
- Definition of Term, Pattern, free variables, binding variables e.t.c. Term.v
- Definition of Swapping operations, freshness and equivariance Swap.v
- Definition of Alpha Equality AlphaEquality.v
- Proofs about Swapping operations SwapProps.v
- Decidability of about Alpha equality AlphaDecider.v
- Other Proofs about Alpha equality AlphaEqProps.v
- Definition and Proofs about alpha renaming AlphaRen.v
- Definition and Proofs about tSubstAux SubstAux.v
- Definition and Proofs about substitution SSubst.v

- 05/17/2014: We now have a web-interface which can be used to lookup our Coq definitions by name.