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>