diff options
| -rw-r--r-- | README.md | 24 |
1 files changed, 23 insertions, 1 deletions
@@ -2,4 +2,26 @@ Various implementations of the lambda calculus (and friends). -The code here is hopefully pretty readable: but makes heavy use of quasiquoting. For an introduction, see [*Explaining Lisp's quoting without getting tangled*](https://cadence.moe/blog/2022-10-17-explaining-lisp-quoting-without-getting-tangled). +The code here is hopefully pretty readable: but makes heavy use of quasiquoting. +For an introduction, see [*Explaining Lisp's quoting without getting tangled*](quasiquoting). + +* [~] LC: The untyped lambda calculus. +* [x] STLC: The simply-typed lambda calculus. +* [x] STLC-ext: Simple extensions. Sums, products, lists, ascryptions. +* [ ] STLC-fix: General recursion. +* [ ] STLC-sub: Subtyping. Structural records, intersective unions, implicit typeclasses, ⊤, ⊥. +* [ ] STLC-rec: Recursive types. Also sums, products, ascryption. +* [x] STLC-ref: References. +* [x] STLC-pred: Higher-order *predicative* references. Terminating. +* [ ] STLC-imp: Higher-order *impredicative* references. Terminating. +* [ ] STLC-rc: References with reference counting. +* [ ] STLC-gc: References with a tracing garbage collector. +* [ ] STLC-own: References with Rust-style ownership. +* [ ] STLC-eff: Effects. +* [ ] STLC-class: Typeclasses +* [~] SKI: The SKI combinator calculus. +* [~] Iota, Jot, Zot: Implementations of Chris Barker's languages. +* [~] Aviary: Various combinators and constructions of equivalence. + + +[quasiquoting]: https://cadence.moe/blog/2022-10-17-explaining-lisp-quoting-without-getting-tangled |