README.md


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

# 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

## Citations

1. Forster, Smolka 2017,
   *Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq*