Abstract

Joint work with Lars Birkedal, Andrew Kennedy and Carsten Varming

We describe a Coq formalization of constructive omega-cpos, ultrametric spaces and ultrametric-enriched categories, up to and including the inverse-limit construction of solutions to mixed-variance recursive equations in both categories enriched over omega-cppos and categories enriched over ultrametric spaces.

We show how these mathematical structures may be used in formalizing semantics for three representative programming languages. Specifically, we give operational and denotational semantics for both a simply-typed CBV language with recursion and an untyped CBV language, establishing soundness and adequacy results in each case, and then use a Kripke logical relation over a recursively-defined metric space of worlds to give an interpretation of types over a step-counting operational semantics for a language with recursive types and general references.