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 > Logic and Semantics Seminar (Computer Laboratory) > Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types

## Realizability Semantics of Parametric Polymorphism, General References, and Recursive TypesAdd to your list(s) Download to your calendar using vCal - Lars Birkedal, ITU Denmark
- Thursday 06 November 2008, 15:30-16:30
- Room FW11, Computer Laboratory, William Gates Building.
If you have a question about this talk, please contact Matthew Parkinson. We present a realizability model for a call-by-value, higher-order programming language with parametric polymorphism, general first-class references, and recursive types. The main novelty is a relational interpretation of open types (as needed for parametricity reasoning) that include general reference types. The interpretation uses a new approach to modeling references. The universe of semantic types consists of world-indexed families of logical relations over a universal predomain. In order to model general reference types, worlds are finite maps from locations to semantic types: this introduces a circularity between semantic types and worlds that precludes a direct definition of either. Our solution is to solve a recursive equation in an appropriate category of metric spaces. In effect, types are interpreted using a Kripke logical relation over a recursively defined set of worlds. Joint work with Kristian Stovring and Jacob Thamsborg This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series. ## This talk is included in these lists:- All Talks (aka the CURE list)
- Cambridge talks
- Computer Laboratory talks
- Computing and Mathematics
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- Room FW11, Computer Laboratory, William Gates Building
- School of Technology
- Trust & Technology Initiative - interesting events
- bld31
- yk373's list
Note that ex-directory lists are not shown. |
## Other listsBioenergy Initiative Inner Space, The Meditation Centre Thin Film Magnetism Group Seminars## Other talks100 Problems around Scalar Curvature Replication or exploration? Sequential design for stochastic simulation experiments Glanville Lecture 2017/18: The Book of Exodus and the Invention of Religion Translational Science: using biomarkers to guide clinical development in oncology A polyfold lab report PTPmesh: Data Center Network Latency Measurements Using PTP “Modulating Tregs in Cancer and Autoimmunity” Throwing light on organocatalysis: new opportunities in enantioselective synthesis Single Cell Seminars (August) Building cortical networks: from molecules to function |