GADT-thesis

This is the repository containing Coq proofs attached to my master's thesis.

Structure of the repository

• lambda2Gmu - my formalization of the source calculus λ2Gμ.
  • Definitions.v define the calculus syntax, typing and semantics and states the desired safety properties.
  • Infrastructure.v proves syntactic properties of binder handling.
  • Regularity.v proves basic properties of the type system, with the most important result - a well typed term has other properties we defined (its type is well formed, it is closed etc.).
  • CanonicalForms.v has proofs that allow to deconstruct a value of a given type to its canonical form.
  • Progress.v proves the progress theorem.
  • Preservation.v proves the preservation theorem.
• lambda2Gmu_annotated - formalization of the annotated variant of the calculus (as described in Section 5.3). The soundness proof is a copy of the standard version with minor adaptations in a few lemmas to accommodate for the added annotations.
• translation_pdot - proofs associated with the translation attempts. Includes lemmas characterizing pDOT's subtyping.
  • RuleTests.v - contains lemmas showing how some too general rules would break soundness.
  • TestEqualityEnv.v - manually translated environment for the Eq GADT.
  • TestEquality.v - typing proofs for coerce and transitivity terms using the Eq GADT.
  • TestEquality3.v - the typing proof for the construct term using the Eq GADT.
• translation_extended - proofs associated with the translation attempts using the extended pDOT calculus.
  • TestEquality.v - typing proofs for coerce and transitivity terms using the Eq GADT.
  • TestEquality2.v - typing proof for the destruct term which was not typeable in original pDOT, as described in Chapter 6.
  • TestEquality3.v - the typing proof for the construct term using the Eq GADT.
• tools contains tools helping with working with the Lambda2Gmu formalization, written in Scala.
  • It features a parser for Lambda2Gmu pseudocode in a human-readable syntax (close to the syntax defined on paper), a transpiler which converts name-based binders to De Bruijn indices and allows to convert the human-readable syntax to Coq terms compatible with the formalization.
  • It features a prototype of the λ2Gμ encoding into pDOT. It parses terms in the annotated variant of λ2Gμ and generates pDOT-pseudocode. An example showing encoded head and zip terms is available in tools/README.md. Encoding of the Σ signature is not implemented yet.

Building the proofs

The proofs require Coq 8.13.0 and the TLC library. The easiest way to obtain them is to use OPAM:

opam repo add coq-released http://coq.inria.fr/opam/released
opam pin add coq 8.13.0
opam install -j4 coq-tlc

The next step is to prepare the dependencies - the standard and extended formalizations of pDOT. This can be done by running the script refresh_dependencies.sh.

Each subproject can be compiled by running make in its corresponding subdirectory. However, the sub-projects depend on each other, so lambda2Gmu should be compiled before lambda2Gmu_annotated and both of these subprojects should be compiled before translation_pdot or translation_extended.

Useful links

• Public repo - the repo where I put finished documents and other deliverables that I want to share
• pDOT repo - formalization of the target calculus, pDOT that I will want to base on
• Localy Nameless library - used for handling binders in calculus proofs, a hybrid approach connecting DeBruijn indices for closed terms and named variables for free terms; using cofinite quantification
• TLC library - a non-constructive library for Coq, used in pDOT proofs (Locally Nameless is a part of it)
• Extended pDOT repo - the repository containing the extended variant of pDOT, as described in Section 6.2.2 of the thesis.

Papers

• A Path to DOT - the paper describing pDOT
• Guarded Recursive Datatype Constructors paper by Xi et al., defining my source calculus