Untyped λ-calculus

md/ULC.All is the root of a section of this website showing an Agda formalization of the denotational semantics of the untyped λ-calulus.

html/ULC.All is the root of the orginal HTML pages generated by Agda from (potentially literate) source code in the GitHub repository.

pdf/ULC.All is a highlighted PDF listing of all the Agda modules.