University of Cambridge > > Semantics Lunch (Computer Laboratory) > Formalizing Domains, Ultrametric Spaces and Semantics of Programming Languages

Formalizing Domains, Ultrametric Spaces and Semantics of Programming Languages

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Sam Staton.

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.

This talk is part of the Semantics Lunch (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity