diff options
Diffstat (limited to 'AUTHORS')
| -rw-r--r-- | AUTHORS | 17 |
1 files changed, 17 insertions, 0 deletions
@@ -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> |