blob: 8247b965d73b274ccee9233aafb7ce5d6dcf9904 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
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>
|
