diff options
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 37 |
1 files changed, 17 insertions, 20 deletions
@@ -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 |