We develop a formal proof of the equivalence of two different variants of System F. The first is close to the original presentation where expressions are separated into distinct syntactic classes of types and terms. The second, L2 (also written as λ2), is a particular pure type system (PTS) where the notions of types and terms, and the associated expressions are unified in a single syntactic class. The employed notion of equivalence is a bidirectional reduction of the respective typing relations. A machine-verified proof of this result turns out to be surprisingly intricate, since the two variants noticeably differ in their expression languages, their type systems and the binding of local variables.
Most of this work is executed in the Coq theorem prover and encompasses a general development of the PTS metatheory, an equivalence result for a stratified and a PTS variant of the simply typed λ-calculus as well as the subsequent extension to the full equivalence result for System F. We utilise nameless de Bruijn syntax with parallel substitutions for the representation of variable binding and develop an extended notion of context morphism lemmas as a structured proof method for this setting.
We also provide two developments of the equivalence result in the proof systems Abella and Beluga, where we rely on higher-order abstract syntax (HOAS). This allows us to compare the three proof systems, as well as HOAS and de Bruijn for the purpose of developing formal metatheory.
This thesis is accompanied by three formalisations in Coq, Abella and respectively Beluga.
All three developments are provided below as source pacakges. Each package has a designated top folder (to avoid pollution of your directory context with arbitrary files) and includes a README.md file. Please consult the README carefully. Note in particular that we recommend the use of opam to install the various proof systems, and moreover multiple "switches" are needed to select the correct OCaml compiler for each of the settings. That is we use OCaml 4.05.0 for Coq and Beluga, while Abella is provisioned for OCaml 4.06.0.
The first and most extensive piece of work is the full PTS development as well as the correspondence proofs for STLC and System F in the Coq Proof assistant, version 8.7.1+1. We provide fully hyperlinked CoqDoc sources in addition to the source package below. Please note that the development depends on the Autosubst framework, version 1. Installation instructions can be found on the corresponding webpage and in the packaged README file.
The first HOAS development is executed with the 2-level logic proof assistant Abella, version 2.0.5. Note that the provided *.sig and *.mod files can also be run using LambdaProlog to query for derivations, including type checking and inference. The equiv.thm file contains the actual equivalence proof.
The second HOAS development is executed in the dependently typed programming language Beluga. Since the latest released version (0.8.2) has a consistency bug in the totality checker for recursive functions (i.e. inductive proofs), we switched to the development version. The proof terms provided below were checked against the master branch of https://github.com/Beluga-lang, which at the time of testing was at commit (285dd31c).