University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > Uncertainty is hope: towards a unified foundation of gradual typing

Uncertainty is hope: towards a unified foundation of gradual typing

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

  • UserJoshua Dunfield, Queen’s University, Canada
  • ClockWednesday 17 April 2019, 14:00-15:00
  • HouseFW26.

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity