Formalizing domain models of the typed and the untyped lambda calculus in Agda
Abstract: We present a domain interpretation of the simply typed and the untyped lambda calculus.The interpretations are constructed using the notion of category with families, with addedstructure. Specifically, for the simply typed case we construct a simply typed categorywith families of (a version of) neighborhood systems with structures supporting binaryproduct types and function types. For the untyped case, we construct a unityped categorywith families of neighborhood systems, with added lambda structure.The work is completely formalized in the dependently typed programming language andproof assistant Agda. The categories with families with added structure are formalizedas records and then instantiated with neighborhood systems as objects and approximablemappings as morphisms. In constructing the appropriate neighborhood system for theuntyped model, we make use of Agda’s sized types; this feature enables us to prove transitivityof the ordering relation between untyped neighborhoods.
AT THIS PAGE YOU CAN DOWNLOAD THE WHOLE ESSAY. (follow the link to the next page)