A solution for the POPLmark challenge

We present a partial solution to the POPLmark Challenge [1] based on Nested Datatypes in the Coq proof assistant. Our formalization addresses part (1A) of the Challenge. This work is a radical improvement of our previous attempt.

The use of the Nested Datatypes to encode higher order syntax is an already established discipline [2][3][4]. Some advantages on using this technique include:

• Typing is refined, taking into account the variation of the set of free variables.

• It is a well-understood concrete approach. There is no alpha-equivalence, which makes life much simpler. In fact, it can be considered the same as the pure de Bruijn encoding under an enlightening typing discipline.

• Substitution is just the so beautiful monadic substitution.

Other random considerations about our formalization:

This formalization is part of our effort to put Modules over Monads and Nested Datatypes at work for reasoning about languages with bindings. The theory supporting our vision is exposed in [3].

Our formalization takes place in the standard Coq environment without axioms or specialized libraries. Yet it is very compact. We estimate the total amount of the information contained in our code by measuring the size of the gzipped sources. We tried to compare the GZib Kbytes size of our code with some other available formalizations. The results obtained are summarized in the following table.

These statistics have been obtained by removing comments and code which does not appear to be necessary for addressing part 1A and by compressing the files with gzip with the option "—best". The whole process has been carried on mostly by hand, which means that it can be affected by errors. Some formalizations are built on top of some kind of general purpose library, in which case we tried to evaluate the size of the library (reported in the column Extras) separately from the size of the code specific for the solution of the Challenge.

This new version is about 5-6 times smaller than our previous attempt published in may 2006. One of the most important difference between the two versions resides in the formalisation of statements involving concatenation of environments. In the new formalization concatenation of environments is not explicitly defined and the notion of relative well-formedness is used instead. For instance, every judgement of the form

Gamma,Delta |- s <: t

has been rephrased systematically by as a conjunction

Delta' |- s <: t      /\      WF Gamma Delta' f

(where Delta' plays the role of Gamma,Delta).

1. The sources for Coq version 8.1: Part1a.v.

2. The html formatted sources: Part1a.html.

3. The source of our earlier solution: fsub-2006-05-19.tar.gz.

• [1] Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Georey Washburn, Stephanie Weirich, and Steve Mechanized Metatheory for the Masses: The PoplMark Challenge. In Proceedings of the Eighteenth International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005). 2005

• [2] Richard Bird and Ross Paterson. De Bruijn Notation as a Nested Datatype. Journal of Functional Programming. 11 p200-222, 1999.

• [3] André Hirschowitz and Marco Maggesi. Modules over Monads and Linearity. WoLLIC 2007. LNCS 4576, p218-237.

• [4] Ralph Matthes. Verification of programs on truly nested datatypes in intensional type theory

• [5] http://www.chargueraud.org/arthur/research/2007/binders/

• [6] http://math.unifi.it/~maggesi/fsub/

• [7] http://cristal.inria.fr/~xleroy/POPLmark/locally-nameless/

• [8] http://alliance.seas.upenn.edu/~plclub/cgi-bin/poplmark/index.php?title=Submission_by_Jérôme_Vouillon