University of Birmingham > Talks@bham > Theoretical computer science seminar > 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 Paul Levy.

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 is joint work with Lars Birkedal, Andrew Kennedy and Carsten Varming.

This talk is part of the Theoretical computer science seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.