# 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*