suzanne.soy/cur
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Added some pointers about what to look at

Browse Source
This commit is contained in:
William J. Bowman 2015-02-05 02:32:50 -05:00
parent b13bf6471d
commit 027f031b20
1 changed files with 18 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
README.md
View File

@ -12,3 +12,21 @@ cur (plural curs)
1. (archaic) A mongrel. 1. (archaic) A mongrel.
2. (archaic) A detestable person. 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.