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.

*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.

Untyped lambda calculus | lambda_calculus | Source | HTML |
---|---|---|---|

lists_decidable | Source | HTML | |

fresh_variables | Source | HTML | |

functions_extra | Source | HTML | |

case_tac | Source | HTML |

- Allen Stoughton. Substitution Revisited. Theor. Comput. Sci., 59: 317-325, 1988.