Proof Pearl: Substitution Revisited, Again
We revisit Allen Stoughton's 1988 paper "Substitution Revisited" and
use it as our test case in exploring a nominal approach to
variable binding in Coq. In our nominal approach, we use only
one-sorted variable names as in pen-and-paper work. We show that it
is not only feasible, but also convenient to work with the nominal
approach in Coq. Furthermore, we figure out a light
infrastructure which provides the base in proving a series of
results about simultaneous substitution and alpha-congruence
in the untyped lambda calculus.
The three main features of our paper are as follows:
- We apply nominal approach with one-sorted variable names to
variable binding in Coq.
- We use Coq's internal equality instead of any kind of
set-theoretic equalities or setoid equalities.
- We employ only Coq's basic terminology and techniques.
Our primary contribution is to demonstrate that it is
not only feasible, but also convenient to work with the
nominal approach in Coq.
Most of all, our formalization is very compact and close to the
original reasoning on paper. We even believe that it would
satisfy the three criteria proposed in POPLmark Challenge, i.e.,
reasonable overheads, cost of entry, and transparency in
evaluating mechanization of formal metatheory. However, this goes
beyond the scope of this paper.
- Proof Pearl: Substitution Revisited, Again.
[Draft]
한글 버전(나현숙과 공동저)은 정보과학회 논문지에 출판되었습니다.
The proof scripts along with required libraries can be downloaded
as a gzip'd tarball [Stoughton.tgz].
Extracting the files creates a directory called Stoughton
which contains six files.
Among them, lambda_calculus.v is the main source code
containing the formalization of (Stoughton 1988).
You can compile the codes and generate all the documents by using
make html.
The proof scripts can be compiled on Coq8.3.pl4.
- Allen Stoughton.
Substitution Revisited.
Theor. Comput. Sci., 59: 317-325, 1988.