From 027f031b20a83830a9e123ab0c83550e9ec064d5 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Thu, 5 Feb 2015 02:32:50 -0500 Subject: [PATCH] Added some pointers about what to look at --- README.md | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/README.md b/README.md index b3c031a..2f4fc34 100644 --- a/README.md +++ b/README.md @@ -12,3 +12,21 @@ cur (plural curs) 1. (archaic) A mongrel. 2. (archaic) A detestable person. ``` + +Getting started +=============== + +Don't actually try to run anything. The type-checker may be exponential, +or worse. + +Open up `stlc.rkt` to see an example of what advanced meta-programming can let you do. + +Open up `oll.rkt` to see the implementation of the meta-programs used to +enable `stlc.rkt`, including the parsers for BNF syntax, inference rule +relation syntax, and Coq and LaTeX generators. + +Open up `proofs-for-free.rkt` to see an implementation of the +translation defined in [Proofs for Free](http://staff.city.ac.uk/~ross/papers/proofs.html) as a meta-program. + +Open up anything in `stdlib/` to see some standard dependent-type +formalisms.