## Some of my early work on the POPLMark ChallengeFrom 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 environmentsThis 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. - Coq source file for POPLMark part 1A
- Documentation of the key ideas from the solution
- Documentation of the details of the definitions, proofs and tactics used
- A few associated slides
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 quantificationThis 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 quantificationThe following developments correspond to a precursor version of the locally nameless approach with cofinite quantification. |