Welcome to the online reference for our LFMTP2014 paper titled "A Generic Approach to Proofs about Substitution"

• 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

Updates

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