# [POPLmark] A "locally nameless" solution in Coq

Xavier Leroy Xavier.Leroy at inria.fr
Mon Oct 10 12:47:36 EDT 2005

```Dear all,

The interesting discussions at ICFP and Merlin two weeks ago finally
motivated me to clean up and put online my (partial) solution to the
POPLmark challenge:

http://cristal.inria.fr/~xleroy/POPLmark/locally-nameless/

This solution covers only part 1a of the challenge (algorithmic
subtyping, no record types).  It is written in Coq, and uses a
"locally nameless" representation for binders: variables bound within
terms are represented by de Bruijn indices, but variables free in
terms are represented by names.  I was inspired by Randy Pollack's
talk, "Reasoning About Languages with Binding":

http://homepages.inf.ed.ac.uk/rap/export/bindingChallenge_slides.pdf

- Alpha-equivalence is term equality, which makes life much simpler in Coq.
- The statements (and even the proofs) of the main theorems are quite
close to what one would write on paper.
- Despite not being completely nominal, it still illustrates some of
the key aspects of fully nominal approaches, especially the
"forall/exists" equivalence for the choice of fresh variables.

- There is a lot of boilerplate involved before getting to the meat
of the proof: two substitution functions (of names and of de Bruijn
variables), computation and properties of free names, swaps,
commutation of swaps with many definitions, the "forall/exists"
theorems, etc.  Consequently, the development is larger than a pure
de Bruijn solution.

- Extending this approach to part 2 of the challenge exceeds my fortitude:
two sorts of names, six substitution functions, even more swaps,
commutation theorems all over the place, ...  Enough is enough  :-)

One good thing about my solution:

- It is heavily commented, then typeset using the coqdoc tool.
Message to my fellow solution submitters: you, too, can write
good English; don't be shy.

- My Coq proof scripts do not have the conciseness and elegance
of Jérôme Vouillon's.  Sorry, I've been using Coq for only 6 years...

Final thoughts:

- If the purpose is just to solve the challenge and be done with it,
I would rather go for pure de Bruijn.
- However, this could change if some of the nominal boilerplate was
built into the logic or at least into the prover.
- The exercise has some educational value, to me at least.

Enjoy,

- Xavier Leroy
```