Lambda-Calculus

The Agda code of a lightweight formalization of the denotational semantics of the untyped lambda-calculus is available on GitHub.

The following highlighted listings of the code were generated using Agda.

• Modules: hyperlinked web pages of the formalization

• Library: hyperlinked web pages of imported standard Agda library modules

• HTML: the hyperlinked HTML pages generated by Agda

• PDF: a PDF listing of the formalization