Generic Reasoning of the Locally Nameless Representation (Artifact)

This is the artifact for the APLAS 2024 paper "Generic Reasoning of the Locally Nameless Representation".

*Update in v3:

1. We have fixed an issue with proofs in the book Practical Foundations for Programming Languages. Please see our notes for more details.
2. We have formalized the proofs in our notes and verification of program equivalence for PCF. These contents are included in the fix_PFPL directory. Please see "README.md" for more details.
3. The  correspondence (denoted by "=") between the theorems mentioned in the notes (bold on the left side of "=") and the ones in Coq files (on the right side of "=") are given as follows:
   • In PcfConverseEvaluation.v: Inverse of Compactness = Lemma fix_m_to_fix_w_step, Generalized Inverse of Compactness = Lemma fix_m_to_fix_w and Generalized Inverse of Compactness for Reduction 1 and 2 = Lemma BandC;
   • In PcfLgDefinition.v: Fixed Point Induction = Lemma fixed_point_induction, Generalized Fixed Point Induction = Lemma general_fixed_point_induction.
4. For consistency, we keep the src directory unchanged.

This artifact contains the Coq implementation of the generic reasoning library for the locally nameless representation and applications of the library, including verification of program equivalence for the simply typed lambda calculus and proving of the compactness theorem for PCF. There is a 'README.md' file in the main directory instructing how to build the code.