blob: 60b3e9aa33fc6b7c0d3e45b33c37de38d8a51f23 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
# 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
## Building
Requirements:
- [rocq](https://rocq-prover.org/)
The project is built with the GNU build system, but skips the
configure step. Building is a one-liner.
```
$ make
```
## Citations
1. Forster, Smolka 2017,
*Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq*
|
