update readme

1 files changed, 23 insertions, 1 deletions

diff --git a/README.md b/README.md
index 798e8a1..e525561 100644
--- a/README.md
+++ b/README.md
@@ -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