blob: d36aef5bde6d4788f8ebd149a163474a8b333b03 (
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
34
35
36
37
38
|
# 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.
```
$ autoconf
$ ./configure
$ make
```
## Installation
See `INSTALL` for instructions.
## Citations
1. Forster, Smolka 2017,
*Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq*
|
