From ad19de6be6b9a9d620d94e3f162dcee1bfda2cf7 Mon Sep 17 00:00:00 2001
From: JJ
Date: Wed, 23 Oct 2024 18:10:03 -0700
Subject: restructure code, put implementations into broadly categorical
 folders

---
 README.md | 37 +++++++++++++++++--------------------
 1 file changed, 17 insertions(+), 20 deletions(-)

(limited to 'README.md')

diff --git a/README.md b/README.md
index 76aadab..3d8b853 100644
--- a/README.md
+++ b/README.md
@@ -2,27 +2,24 @@
 
 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*](quasiquoting).
+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*](quasiquoting). For an introduction to contracts, see [*Simple contracts on functions*](https://docs.racket-lang.org/guide/contract-func.html).
 
-* [~] LC: The untyped lambda calculus.
-* [x] STLC: The simply-typed lambda calculus.
-* [x] STLC-ext: Simple extensions. Sums, products, lists, ascryptions.
-* [x] STLC-fix: General recursion.
-* [x] STLC-rec: Iso-recursive types.
-* [ ] STLC-sub: Subtyping. Structural records, intersective unions, implicit typeclasses, ⊤, ⊥.
-* [x] STLC-ref: References.
-* [x] STLC-pred: Higher-order *predicative* references. Terminating.
-* [x] STLC-imp: Higher-order *impredicative* references. Terminating.
-* [x] STLC-dll: Doubly-linked lists via sums, products, ascryption, recursive types, and impredicative references. Terminating?
-* [ ] STLC-rc: References with reference counting.
-* [ ] STLC-gc: References with a tracing garbage collector.
-* [ ] STLC-own: References with first-class ownership, Rust-style.
-* [ ] STLC-lent: References with second-class ownership.
-* [ ] STLC-dep: Dependent types with normalization by evaluation.
-* [~] SKI: The SKI combinator calculus.
-* [~] Iota, Jot, Zot: Implementations of Chris Barker's languages.
-* [~] Aviary: Various combinators and constructions of equivalence.
+* 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?
 
 
 [quasiquoting]: https://cadence.moe/blog/2022-10-17-explaining-lisp-quoting-without-getting-tangled
-- 
cgit v1.2.3-70-g09d2