Formalizing Domains, Ultrametric Spaces and Semantics of Programming Languages

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

• Nick Benton, Microsoft Research Cambridge
• Friday 21 January 2011, 16:00-17:00
• UG40 Computer Science.

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.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• UG40 Computer Science
• computer sience

Note that ex-directory lists are not shown.