Untyped λ-calculus

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

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

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