Write a Blog >>
Sat 25 Jan 2020 09:00 - 09:30 at Orleans - Gradual Criteria Chair(s): Amal Ahmed

Gradual typing is a principled approach to integrating static and dynamic type checking. To clarify what gradual typing means, Siek and collaborators articulated criteria for gradually typed languages: essentially that type checking and execution must smoothly transition between the two type checking regimes. However, these criteria say nothing about the relationship between the semantics of gradual and static types. This absence, which can be ascribed to gradual typing’s tendency to focus on simple types, becomes critical for advanced type disciplines, where type \emph{safety} does not imply type \emph{soundness}.

We assert a semantic criterion for gradual types. To coherently blend static and dynamic checking of a particular type discipline, a gradual type system must enforce the same invariants as those \emph{intended} by its purely-static counterpart. We justify this stance by considering several type disciplines, highlighting key challenges and opportunities.

Sat 25 Jan
Times are displayed in time zone: Saskatchewan, Central America change

09:00 - 10:00: Gradual CriteriaWGT at Orleans
Chair(s): Amal AhmedNortheastern University, USA
09:00 - 09:30
Gradual Typing as if Types Mattered
Ronald GarciaUniversity of British Columbia, Éric TanterUniversity of Chile
09:30 - 10:00
Fully Abstract from Static to Gradual
Koen JacobsKU Leuven, Amin Timanyimec-Distrinet KU-Leuven, Dominique DevrieseVrije Universiteit Brussel