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