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 Types

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2020 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity