Lambda v0.0.0v0.0.0

1 files changed, 17 insertions, 0 deletions

diff --git a/AUTHORS b/AUTHORS
new file mode 100644
index 0000000..8247b96
--- /dev/null
+++ b/AUTHORS
@@ -0,0 +1,17 @@
+Lambda is a Rocq library used for writing proofs about the untyped
+lambda calculus. It grew from an exercise in working through Forster
+and Smolka's 2017 paper "Weak Call-by-Value Lambda Calculus as a Model
+of Computation in Coq."
+
+The proofs in the original paper can be found at
+
+https://www.ps.uni-saarland.de/extras/L-computability/
+
+whose authors were 
+
+Yannick Forster <forster@ps.uni-saarland.de>
+Gert Smolka <smolka@ps.uni-saarland.de>
+
+The additional proofs or rewrites contained here were made by
+
+Daniel Rostovtsev <dan@rostovtsev.org>