Some of my early work on the POPLMark Challenge

From March to July 2006, I have been working on the POPLmark Challenge at the University of Pennsylvania, with Benjamin Pierce and Stephanie Weirich as advisors.

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.