suzanne.soy/cur
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
Powerful meta-programming for powerful types.
91 Commits 29 Branches 0 Tags 790 KiB
Racket 100%
3ce14c3871
Go to file
William J. Bowman 3ce14c3871
Refactored core 
Moved all curnel code into curnel/, and split the two kernel modules
into separate files. Now the trusted core and the module/#lang stuff are
in separate files. The #lang is now reprovided by "cur.rkt", which
should also provide core agnostic sugar.
2015-09-15 18:02:36 -04:00
curnel Refactored core 2015-09-15 18:02:36 -04:00
stdlib Refactored core 2015-09-15 18:02:36 -04:00
cur.rkt Refactored core 2015-09-15 18:02:36 -04:00
example.rkt Refactored core 2015-09-15 18:02:36 -04:00
LICENSE Updated LICENSE to BSD 2-clause 2015-09-15 16:12:15 -04:00
oll.rkt Refactored core 2015-09-15 18:02:36 -04:00
proofs-for-free.rkt Refactored core 2015-09-15 18:02:36 -04:00
README.md Refactored core 2015-09-15 18:02:36 -04:00
stlc.rkt Refactored core 2015-09-15 18:02:36 -04:00

README.md

cur

A language with static dependent-types and dynamic types, type annotations and parentheses, theorem proving and meta-programming.

Noun
cur (plural curs)

1. (archaic) A mongrel.
2. (archaic) A detestable person.

Getting started

Requires redex-lib version 1.6 if you want answers in a reasonable amount of time. Otherwise, the type-checker may require exponential time 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 and inference rule syntax, and Coq and LaTeX generators.

Open up proofs-for-free.rkt to see an implementation of the translation defined in Proofs for Free as a meta-program.

Open up anything in stdlib/ to see some standard dependent-type formalisms.

Open up curnel/redex-core.rkt to see the entire "trusted" (after a large test suite) core.