blob: 3d8b853c3eb1dfa5d25a3ff3aa51f284e4d9e5ed (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
# 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*](quasiquoting). For an introduction to contracts, see [*Simple contracts on functions*](https://docs.racket-lang.org/guide/contract-func.html).
* 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
|
