the mechanicals

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
• [x] stlc.rkt: The simply-typed lambda calculus.
• [x] ext.rkt: Simple extensions. Sums, products, lists, ascryptions.
• [x] fix.rkt: General recursion.
• [x] rec.rkt: Iso-recursive types.
• [x] ref.rkt: References. No garbage collection. Nonterminating.
• research
• [x] hor.rkt: Higher-order im/predicative references. Terminating.
• [x] dll.rkt: Doubly-linked lists via sums, products, ascryption, recursive types, and impredicative references. Terminating?
• [x] levels.rkt: Higher-order im/predicative references with an algebraic level system. Terminating?