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

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

• Philip Wadler, University of Edinburgh
• Tuesday 14 March 2023, 14:00-15:00
• SS03, Computer Laboratory.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• SS03, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• tcw57’s list
• yk373's list

Note that ex-directory lists are not shown.