Formalizing Domains, Ultrametric Spaces and Semantics of Programming Languages

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

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

This is joint work with Lars Birkedal, Andrew Kennedy and Carsten Varming.