Description of our formalization
We present [4] 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][5]. 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.
| Contribution | Part 1A | Extras |
|---|---|---|
| B.Aydemir et al. [6] | 2.5 Kb | 16.4 Kb |
| A.Hirschowitz & M.Maggesi 2.7 K | b 0 Kb | |
| X.Leroy [7] | 5.0 Kb | 1.0 Kb |
| J.Vouillon [8] | 4.6 Kb | 0 Kb |
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 <: thas been rephrased systematically by as a conjunction
Delta' |- s <: t /\ WF Gamma Delta' f(where Delta' plays the role of Gamma,Delta).
Source code
-
The sources for Coq version 8.1: Part1a.v.
-
The html formatted sources: Part1a.html.
-
The source of our earlier solution: fsub-2006-05-19.tar.gz.
Paper
For a detailed description we refer to our paper [4] (also available online).
References
-
[1] Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn,
-
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 (website)
-
-
[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] André Hirschowitz and Marco Maggesi. Nested Abstract Syntax in Coq. Journal of Automated Reasoning'. October 2012, Volume 49, Issue 3, pp 409-426 pdf
-
[5] Ralph Matthes. Verification of programs on truly nested datatypes in intensional type theory