An interactive tutorial on specifying and implementing the simply-typed lambda calculus in Coq.
This tutorial depends on the
Metalib.Metatheory library, available from
Make sure that you compile and install this library first.
After you have done that, you can use make to compile the tutorial material and generate the documentation.
`make` - Compile all Coq files `make html` - Make documentation
Read through the tutorial files in this order. Some files have embedded
exercises; their solutions are in the associated
Lec1.v - First set of lecture notes, with exercises about LN Definitions.v - Specification of STLC using locally nameless representation (LN) Lec2.v - LN continued: type soundness for STLC Lemmas.v - Auxiliary lemmas about LN, generated by LNgen tool Nominal.v - Definition of STLC using nominal representation, abstract machine based small-step semantics Connect.v - Proof that nominal abstract machine implements LN substitution-based small-step semantics
Warning: the exercises start simple, but ramp up. The first two exercise files have significantly simpler exercises than the second two files.
stlc.ott - Ott specification of STLC stlc.mng - LaTeX source gen.mk - Makefile recipes for invoking Ott/LNgen/LaTex stlc.pdf - PDF version of rules Stlc.v - Ott-generated version of `Definitions.v` Stlc_inf.v - LNgen generated version of `Lemmas.v`
If you have Ott and LNgen installed, you may also generate the files above.
`make -f gen.mk stlc.pdf` `make -f gen.mk Stlc.v` `make -f gen.mk Stlc_inf.v`
Tutorial author: Stephanie Weirich, based on prior a tutorial by Brian Aydemir and Stephanie Weirich, with help from Aaron Bohannon, Nate Foster, Benjamin Pierce, Jeffrey Vaughan, Dimitrios Vytiniotis, and Steve Zdancewic. Adapted from code by Arthur Chargu'eraud.