Uncertainty is hope: towards a unified foundation of gradual typing

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

• Joshua Dunfield, Queen’s University, Canada
• Wednesday 17 April 2019, 14:00-15:00
• FW26.

If you have a question about this talk, please contact Victor Gomes.

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.

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
• FW26
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.