Skip to content

Latest commit

 

History

History
49 lines (34 loc) · 1.71 KB

README.md

File metadata and controls

49 lines (34 loc) · 1.71 KB

STLC Tutorial using Locally Nameless representation

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

Copied from https://github.com/DeepSpec/dsss17/tree/master/Stlc

Installation

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

Contents

Read through the tutorial files in this order.

 Lec1.v            - First set of lecture notes
 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

Extra

The extra directory 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.