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 added structure. Specifically, for the simply typed case we construct a simply typed category with families of (a version of) neighborhood systems with structures supporting binary product types and function types. For the untyped case, we construct a unityped category with families of neighborhood systems, with added lambda structure. The work is completely formalized in the dependently typed programming language and proof assistant Agda. The categories with families with added structure are formalized as records and then instantiated with neighborhood systems as objects and approximable mappings as morphisms. In constructing the appropriate neighborhood system for the untyped model, we make use of Agda’s sized types; this feature enables us to prove transitivity of the ordering relation between untyped neighborhoods.