Taming the Merge Operator: A Type-Directed Operational Semantics Approach
- simple/coq/ for Coq formalization of the λi calculus
- simple/spec/ for Ott specification of the λi calculus
- plus/coq/ for Coq formalization of the λi+ calculus
- plus/spec/ for Ott specification of the λi+ calculus
Our Coq proofs are verified in Coq 8.11.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.
-
Install Coq 8.11.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. -
Make sure
Coq
is installed (typecoqc
in the terminal, if you see "command not found" this means you have not properly installed Coq), then installMetalib
:- Open terminal
git clone https://github.com/plclub/metalib
cd metalib/Metalib
- Make sure the version is correct by
git checkout 04b7aeaf82ceb7e00e1e456fc9fea20a85e09f6f
make install
-
Enter either simple/coq/ or plus/coq/directory.
-
Type
make
in the terminal to build and compile the proofs. -
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
-
syntax_ott.v
,rules_inf.v
, andrules_inf2.v
(in simple/coq/) are generated by Ott and LNgen. Runmake ottclean
to remove them. Thenmake
can reproduce the code (with Ott and LNgen installed).
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
(andrules_inf2.v
) contains thelngen
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).