![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Philip Wadler, University of Edinburgh
Tuesday 14 March 2023, 14:00-15:00
Graduality and Parametricity - Together again for the first time, for the second time
- đ¤ Speaker: Philip Wadler, University of Edinburgh
- đ Date & Time: Tuesday 14 March 2023, 14:00 - 15:00
- đ Venue: SS03, Computer Laboratory
Abstract
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.
Series This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.
Included in Lists
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- Computing and Mathematics
- Department of Computer Science and Technology talks and seminars
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- Martin's interesting talks
- School of Technology
- SS03, Computer Laboratory
- tcw57âs list
- Trust & Technology Initiative - interesting events
- yk373's list
- yk449
Note: Ex-directory lists are not shown.