Some of my early work on the POPLMark Challenge
Three particular approaches to the POPLMark challenge are described below. Note that all of this work is subsumed by our later work on the Locally Nameless library (LN).
Solution 1: de-Bruijn indices and implicit environments
This is a solution to Part 1A of the POPLmark challenge. Bound and free variables are represented with de-Bruijn indices. Well-formedness hypotheses are kept at the root of the derivations. Bound variables are labelled with the type they are bound to in the environment, thus making the environments implicit.
This work has been greatly influanced by Jérome Vouillon's solution, and also some tactics and methods from Xavier Leroy's code were used.
Solution 2: locally nameless, with universal quantification
This is a solution to Part 1A of the POPLmark challenge. It is based on a locally nameless encoding. Bound variables are represented with their de-Bruijn indices, and free variables are represented with names. Well-formedness hypotheses are kept at the root of the derivations. Names introduced are quantified as 'forall x' instead of the standard 'exists x # E'. The consequence is that we have to release the constraint of functionality of environments.
This solution has not been shown to be fully adequate. It is to be considered as an intermediate step towards solution 3.
Solution 3: locally nameless, with a cofinite quantification
The following developments correspond to a precursor version of the locally nameless approach with cofinite quantification.