meow

4 files changed, 65 insertions, 2 deletions

diff --git a/plt/continuations.md b/plt/continuations.md
index b1566d0..096e0c3 100644
--- a/plt/continuations.md
+++ b/plt/continuations.md
@@ -5,12 +5,18 @@ title: computation/continuations
 
 # continuations
 
-- [nim-works CPS](https://github.com/nim-works/cps/tree/master/docs):
+- ✨ [Deliminated Continuations, Demystified](https://www.youtube.com/watch?v=TE48LsgVlIU): 45-minute talk explaining native first-class deliminated continuations - and everything else along the way
+- ✨ [Oleg Kiselyov's writings](https://okmij.org/ftp/continuations/)
+- [nim-works CPS](https://github.com/nim-works/cps/tree/master/docs)
 - [CPS vs. SSA](http://www.mlton.org/pipermail/mlton/2003-January/023054.html)
 - [By example: continuation-passing style](https://matt.might.net/articles/by-example-continuation-passing-style/)
 - [How to compile with continuations](https://matt.might.net/articles/cps-conversion/)
-- [**Oleg Kiselyov's writings**](https://okmij.org/ftp/continuations/)
 - [An argument against call/cc](https://okmij.org/ftp/continuations/against-callcc.html)
+- [Compiling with Continuations](https://annas-archive.org/md5/ce6c60adc8597d750a1f2b7f5023e207)
+- [The Essence of Compiling with Continuations](https://dl.acm.org/doi/pdf/10.1145/173262.155113)
+- [Compiling with Continuations, Continued](../papers/1291151.1291179.pdf)
+- [Compiling without Continuations](https://dl.acm.org/doi/pdf/10.1145/3062341.3062380)
+- [Compiling with Continuations, or without? Whatever.](https://dl.acm.org/doi/pdf/10.1145/3341643)
 
 ## continuations
 
diff --git a/plt/index.md b/plt/index.md
index 8cd6a05..2f5da20 100644
--- a/plt/index.md
+++ b/plt/index.md
@@ -3,4 +3,30 @@ layout: plt
 title: programming language theory
 ---
 
+<br>
+<br>
+<br>
+<br>
+<br>
+
 # programming language theory
+
+constructs
+- [types](types)
+- [continuations](continuations)
+- [effects](effects)
+- [modules](modules)
+- monads
+
+formalisms
+- syntax
+- semantics
+- formal verification
+- paradigms
+
+computation
+- propositions as types
+- [the lambda calculus](lambda-calculus)
+- turing machines
+- [interaction nets](interaction-nets)
+- combinators
diff --git a/plt/interaction-nets.md b/plt/interaction-nets.md
new file mode 100644
index 0000000..c5ce362
--- /dev/null
+++ b/plt/interaction-nets.md
@@ -0,0 +1,11 @@
+---
+layout: plt
+title: computation/interaction nets
+---
+
+# interaction nets
+
+- [xxiivv](https://wiki.xxiivv.com/site/interaction_nets.html)
+- [Interaction nets](https://dl.acm.org/doi/pdf/10.1145/96709.96718)
+- [An algorithm for optimal lambda calculus reduction](https://dl.acm.org/doi/pdf/10.1145/96709.96711)
+- [Optimality and inefficiency: what isn't a cost-model of the lambda calculus?](https://dl.acm.org/doi/pdf/10.1145/232629.232639)
diff --git a/plt/lambda-calculus.md b/plt/lambda-calculus.md
index b666ef6..7d15dbf 100644
--- a/plt/lambda-calculus.md
+++ b/plt/lambda-calculus.md
@@ -4,3 +4,23 @@ title: computation/lambda calculus
 ---
 
 # the lambda calculus
+
+the lambda calculus is a simple expression of computation.
+
+```racket
+;; A full implementation of the untyped lambda calculus in Racket.
+(define (interpret expr [ctx #hash()])
+  (match expr
+    [val #:when (value? val) val]
+    [val #:when (symbol? val)
+      (if (dict-has-key? ctx val)
+        (interpret (dict-ref ctx val) ctx) val)]
+    [`(λ ,id ,body) `(λ ,id ,body)]
+    [`(,body ,arg)
+      (match (interpret body ctx)
+        [`(λ ,id ,body) (interpret body (dict-set ctx id (interpret arg ctx)))]
+        [expr `(,(interpret expr ctx) ,(interpret arg ctx))])]
+    [expr (error (format "invalid expression ~a" expr))]))
+```
+
+in computer science, the lambda calculus is often used as a base for languages and types systems for its simplicity and extended with syntax and types of various fashions. in linguistics, the lambda calculus is used for its compact notation of functions and is often extended with quantifiers and abstract functions. in mathematics, the lambda calculus is studied in its own right.