BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formalizing Domains\, Ultrametric Spaces and Semantics of Programm
 ing Languages - Nick Benton
DTSTART:20101206T124500Z
DTEND:20101206T140000Z
UID:TALK27338@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:Joint work with Lars Birkedal\, Andrew Kennedy and Carsten Var
 ming\n\nWe describe a Coq formalization of constructive omega-cpos\, ultra
 metric spaces and\nultrametric-enriched categories\, up to and including t
 he inverse-limit construction of\nsolutions to mixed-variance recursive eq
 uations in both categories enriched over omega-cppos\nand categories enric
 hed over ultrametric spaces.\n\nWe show how these mathematical structures 
 may be used in formalizing semantics for\nthree representative programming
  languages. Specifically\, we give operational and\ndenotational semantics
  for both a simply-typed CBV language with recursion and an\nuntyped CBV l
 anguage\, establishing soundness and adequacy results in each case\, and\n
 then use a Kripke logical relation over a recursively-defined metric space
  of worlds to\ngive an interpretation of types over a step-counting operat
 ional semantics for a language\nwith recursive types and general reference
 s.\n\n
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR