Skip to content

Latest commit

 

History

History
69 lines (50 loc) · 2.75 KB

README.md

File metadata and controls

69 lines (50 loc) · 2.75 KB
Raw

An interactive tutorial on specifying and implementing the simply-typed lambda calculus in Coq.

INSTALLATION

This tutorial depends on the Metalib.Metatheory library, available from this repository. Make sure that you compile and install the library first.

After you have done that, you can use make to compile the tutorial material split out the solutions, and generate the documentation.

`make`                  - Split solutions and compile all Coq files
`make html`             - Make documentation

SPLITTING

Some of the files in this tutorial include exercises and the solutions to those exercises are embedded in the files. If you want to go through this tutorial in "tutorial mode", you should look at the _full.v versions of the file. To see a cleaned up version of the solutions check out the _sol.v version.

CONTENTS

Read through the tutorial files in this order. Some files have embedded exercises; their solutions are in the associated _sol.v file.

 Lec1_full.v       - First set of lecture notes, with exercises
                     about LN
 Definitions.v     - Specification of STLC using locally nameless
                     representation (LN)
 Lec2_full.v       - LN continued: type soundness for STLC
 Lemmas.v          - Auxiliary lemmas about LN, generated by LNgen tool
 Nominal_full.v    - Definition of STLC using nominal representation,
                     abstract machine based small-step semantics
 Connect_full.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.

EXTRA

This directory also includes files and recipes that were used to generate the some of the above definitions and lemmas, using the Ott and LNgen tools.

 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`

CREDITS

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.