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