University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Graduality and Parametricity - Together again for the first time, for the second time

Graduality and Parametricity - Together again for the first time, for the second time

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

If you have a question about this talk, please contact Jamie Vicary.

Gradual types are essential: they support users of untyped languages to migrate to typed languages, and users of typed languages to migrate to more strongly typed languages. The gradual guarantee (graduality for short) is the key property that relates the semantics of less stongly typed and more strongly typed code.

Polymorphic types are essential. They are at the core of every typed functional language, from ML to Caml to Haskell, and are one key ingredient of dependently typed languages, from Coq to Agda to Idris. Parametricity is the key property that governs the semantics of polymorphic types.

Alas, graduality and parametricity are known to be at odds, as explored in a string of work by Igarashi et al (2017), New at al (2020), and Labrada et al (2022). (We steal our title from the second of these.) Here we propose a new solution combining ideas from all three.

Joint work with Jeremy Siek and Peter Thiemann.

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-2024 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity