Skip to main content
Home

Main navigation

  • Home
  • Series
  • People
  • Depts & Colleges
  • Open Education

Main navigation

  • Home
  • Series
  • People
  • Depts & Colleges
  • Open Education

Gradual Typing with Union and Intersection Types

Series
International Conference on Functional Programming 2017
Video Embed
Victor Lanvin (ENS Cachan, France) gives the third talk in the fourth panel, Integrating Static and Dynamic Typing, on the 3rd day of the ICFP conference.
Co-written by Giuseppe Castagna (CNRS, University of Paris Diderot).

We propose a type system for functional languages with gradual types and set-theoretic type connectives and prove its soundness. In particular, we show how to lift the definition of the domain and result type of an application from non-gradual types to gradual ones and likewise for the subtyping relation. We also show that deciding subtyping for gradual types can be reduced in linear time to deciding subtyping on non-gradual types and that the same holds true for all subtyping-related decision problems that must be solved for type inference. More generally, this work not only enriches gradual type systems with unions and intersections and with the type precision that arise from their use, but also proposes and advocates a new style of gradual types programming where union and intersection types are used by programmers to instruct the system to perform fewer dynamic checks.

More in this series

View Series
International Conference on Functional Programming 2017

On Polymorphic Gradual Typing

Yuu Igarashi (Kyoto University, Japan) gives the second talk in the fourth panel, Integrating Static and Dynamic Typing, on the 3rd day of the ICFP conference.
Previous
International Conference on Functional Programming 2017

Constrained Type Families

Richard A. Eisenberg (Bryn Mawr College, USA) gives the first talk in the fifth panel, Inference and Analysis, on the 3rd day of the ICFP conference.
Next
Licence
Creative Commons Attribution-Non-Commercial-Share Alike 2.0 UK: England & Wales; http://creativecommons.org/licenses/by-nc-sa/2.0/uk/

Episode Information

Series
International Conference on Functional Programming 2017
People
Victor Lanvin
Keywords
technology
computing
programming
Department: Department of Computer Science
Date Added: 23/01/2018
Duration: 00:17:31

Subscribe

Apple Podcast Video Video RSS Feed

Download

Download Video

Footer

  • About
  • Accessibility
  • Contribute
  • Copyright
  • Contact
  • Privacy
'Oxford Podcasts' Twitter Account @oxfordpodcasts | MediaPub Publishing Portal for Oxford Podcast Contributors | Upcoming Talks in Oxford | © 2011-2022 The University of Oxford