aboutsummaryrefslogtreecommitdiff
path: root/README.md
diff options
context:
space:
mode:
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*