Various implementations of the lambda calculus (and friends).
The code here is hopefully pretty readable: but makes heavy use of quasiquoting, and contracts.
For an introduction to quasiquoting, see Explaining Lisp's quoting without getting tangled. For an introduction to contracts, see Simple contracts on functions.
- untyped
- lc.rkt: The untyped lambda calculus.
- ski.rkt: The SKI combinator calculus.
- iota.rkt, jot.rkt, zot.rkt: Implementations of Chris Barker's combinator languages.
- aviary.rkt: Various combinators and constructions of equivalence.
- simple
- stlc.rkt: The simply-typed lambda calculus.
- ext.rkt: Simple extensions. Sums, products, lists, ascryptions.
- fix.rkt: General recursion.
- rec.rkt: Iso-recursive types.
- ref.rkt: References. No garbage collection. Nonterminating.
- research
- hor.rkt: Higher-order im/predicative references. Terminating.
- dll.rkt: Doubly-linked lists via sums, products, ascryption, recursive types, and impredicative references. Terminating?
- levels.rkt: Higher-order im/predicative references with an algebraic level system. Terminating?