This is the Coq formalization of paper Taming the Merge Operator, in the Journal of Functional Programming.

Code Structure

• simple for the λ_i calculus
• plus for the λ_i⁺ calculus present in JFP
• plus_flex_proj for the enhanced λ_i⁺ calculus present in thesis
• pair_simple for the λ_i calculus plus product types and pairs

Each directory contains a sub-directory for Coq formalization and a sub-directory for Ott specification.

Building Instructions

Our Coq proofs are verified in Coq 8.14.1. We rely on two Coq libraries: metalib for the locally nameless representation in our proofs; and LibTactics.v, which is included in the directory.

Prerequisites

0. ott and lngen are used to generate syntax_ott.v and rules_inf.v. You can run all code without them installed unless you want to modify the definitions. In that cases you can refer to the instructions:

   • Ott
   • LNgen

   If you install lngen via cabal and want to be able to call it directly, you may have to change your $PATH, e.g., export PATH=$HOME/.cabal/bin:$PATH.

1. Install Coq 8.14.1. The recommended way to install Coq is via OPAM. Refer to here for detailed steps. Or one could download the pre-built packages for Windows and MacOS via here. Choose a suitable installer according to your platform.

2. Make sure Coq is installed (type coqc in the terminal, if you see "command not found" this means you have not properly installed Coq), then install Metalib:

   1. Open terminal
   2. git clone https://github.com/plclub/metalib
   3. cd metalib/Metalib
   4. Make sure the version is correct by git checkout be0f81cd12ee0e6e06863339cd3ee562dd94aaf9 (other versions may also work)
   5. make install

Build and Compile the Proofs

1. Enter either simple/coq/ or plus/coq/directory.

2. Type make in the terminal to build and compile the proofs.

3. You should see something like the following (suppose > is the prompt):

   coq_makefile -arg '-w -variable-collision,-meta-collision,-require-in-module' -f _CoqProject -o CoqSrc.mk
   COQDEP VFILES
   COQC LibTactics.v
   COQC syntax_ott.v
   COQC rules_inf.v
   COQC Subtyping_inversion.v
   COQC Infrastructure.v
   COQC Deterministic.v
   COQC Type_Safety.v

4. syntax_ott.v, rules_inf.v, and rules_inf2.v (in simple/coq/) are generated by Ott and LNgen. Run make ottclean to remove them. Then make can reproduce the code (with Ott and LNgen installed).

Proof Structure

• syntax_ott.v contains the locally nameless definitions of the calculi and Dunfield's calculus. It involves the typing and semantics of the calculi, the semantics of Dunfield's calculus, and the typing of lambdai (icfp2016). One unified definition of type is used. The last two share the same set of expressions (dexp).
• rules_inf.v (and rules_inf2.v) contains the lngen generated code.
• Infrastructure.v contains the type systems of the calculi and some lemmas.
• Subtyping_inversion.v contains some properties of the subtyping relation.
• Key_properties.v constains some necessary lemmas about typed reduction, top-like relation and disjointness.
• Deterministic.v contains the proofs of the determinism property.
• Type_Safety.v contains the proofs of the type preservation and progress properties.
• dunfield.v (in simple/coq/) contains the proofs of the soundness theorem with respect to Dunfield's calculus.
• icfp.v(in simple/coq/) contains the proofs of the completeness theorem with respect to lambdai (icfp2016).