aboutsummaryrefslogtreecommitdiff
path: root/README.md
diff options
context:
space:
mode:
authorDan Rostovtsev <dan@rostovtsev.org>2026-03-29 15:32:40 -0400
committerDan Rostovtsev <dan@rostovtsev.org>2026-03-29 15:32:40 -0400
commitfb9d9ed9995c6e411f1223d5b53f7b8b6880573e (patch)
tree3ae3d28a9f1b575495fee2b65baa619e8929027f /README.md
Simple build and README.
Diffstat (limited to 'README.md')
-rw-r--r--README.md20
1 files changed, 20 insertions, 0 deletions
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..19c9833
--- /dev/null
+++ b/README.md
@@ -0,0 +1,20 @@
+# Lambda
+
+Fundamental objects and results in the untyped lambda calculus.
+
+Based off of the untyped weak call-by-value lambda calculus in [1].
+
+## Main Features
+
+- Weak Call-by-Value Lambda Calculus
+
+- Beta-Reduction
+
+- Church-Rosser Properties
+
+- Uniform Confluence
+
+## Citations
+
+1. Forster, Smolka 2017,
+ *Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq*