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

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