COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

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

## Formalizing Domains, Ultrametric Spaces and Semantics of Programming LanguagesAdd to your list(s) Download to your calendar using vCal - Nick Benton
- Monday 06 December 2010, 12:45-14:00
- Room FW26, Computer Laboratory, William Gates Building.
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. ## This talk is included in these lists:- All Talks (aka the CURE list)
- Cambridge talks
- Department of Computer Science and Technology talks and seminars
- Interested Talks
- Room FW26, Computer Laboratory, William Gates Building
- School of Technology
- Semantics Lunch (Computer Laboratory)
- Trust & Technology Initiative - interesting events
- bld31
- yk373's list
Note that ex-directory lists are not shown. |
## Other listsComputer Science Essentials Imaging and Mathematics Lucy Cavendish College## Other talksMigration in Science CANCELLED - Methodology Masterclass: Exploring the pedagogic possibilities of new diaspora formations and transnationalism. Development of a Broadly-Neutralising Vaccine against Blood-Stage P. falciparum Malaria What is the Market Potential of Multilingualism? CANCELLED - Mathematical methods in reacting flows: From spectral to Lyapunov analysis Finding the past: Medieval Coin Finds at the Fitzwilliam Museum A transmissible RNA pathway in honeybees Atiyah Floer conjecture Cambridge - Corporate Finance Theory Symposium September 2017 - Day 2 The Anne McLaren Lecture: CRISPR-Cas Gene Editing: Biology, Technology and Ethics Sneks long balus MicroRNAs as circulating biomarkers in cancer |