Rewriting Logic Semantics of Lambda Calculus

From FSL

The Lambda calculus is a simple language calculus that provides a functional model of computation. Many functional programming languages have used the ideas from the lambda calculus as a base, and many proofs in programming languages are carried out on various versions of the lambda calculus.

[edit] Current Release

Our current release is version 1.00 of the untyped lambda calculus. We provide several substitution models, including a standard model of substitution and two weaker models which will not always work but are useful for exploring what can go wrong when substitution is not performed correctly. Multiple methods of reduction, including normal-order and applicative order, are also provided. Finally, support for using de Bruijn indices is included, and a number of macros are provided to make using the definition easier (a definition of plus on Church numerals, for instance, which is expanded to the proper lambda term automatically).

• untyped lambda calculus, in Maude: lambda.maude

Hopefully additional variants will be posted soon, including (especially) the simply typed lambda calculus.