Uncertainty is hope: towards a unified foundation of gradual typing
- π€ Speaker: Joshua Dunfield, Queenβs University, Canada
- π Date & Time: Wednesday 17 April 2019, 14:00 - 15:00
- π Venue: FW26
Abstract
Classic gradual type systems support incremental migration between static typing and dynamic typing. In the last few years, gradual typing has expanded to support incremental migration between ordinary static typing and more precise typing disciplines. Gradual sum types (POPL ‘17) support migration between ordinary static typing and a form of refinement type.
To go beyond ``one-off’’ gradual type systems, we need to unify the foundations of gradual typing. The essence of gradual typing is uncertainty; we propose to isolate uncertainty in a single binary connective, the diamond type, which is a merger of intersection and union types. We explore whether this new connective could provide a foundation for gradual typing that encompasses several existing gradual typing features, including the classic unknown type `?’, gradual sums, and gradual unions.
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
- FW26
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- Martin's interesting talks
- School of Technology
- tcw57βs list
- Trust & Technology Initiative - interesting events
- yk373's list
- yk449
Note: Ex-directory lists are not shown.
![[Talks.cam]](/static/images/talkslogosmall.gif)

Joshua Dunfield, Queenβs University, Canada
Wednesday 17 April 2019, 14:00-15:00