A simple blame calculus for explicit nulls
Gradual typing provides a model for when a legacy language with less precise types interacts with a newer language with more precise types. Casts mediate between types of different precision, allocating blame when a value fails to conform to a type. The blame theorem asserts that blame always falls on the less-precisely typed side of a cast. One instance of interest is when a legacy language (such as Java) permits null values at every type, while a newer language (such as Scala or Kotlin) explicitly indicates which types permit null values. Nieto et al. in 2020 introduced a gradually typed calculus for just this purpose. The calculus requires three distinct constructors for function types and a non-standard proof of the blame theorem; it can embed terms from the legacy language into the newer language (or vice versa) only when they are closed. Here, we define a simpler calculus that is more orthogonal, with one constructor for function types and one for possibly nullable types, and with an entirely standard proof of the blame theorem; it can embed terms from the legacy language into the newer language (and vice versa) even if they are open. All results in the paper have been mechanized in Coq.
Tue 14 OctDisplayed time zone: Perth change
10:50 - 12:05 | Gradual Typing and SecurityICFP Papers / JFP First Papers at Orchid Plenary Ballroom Chair(s): Jeremy G. Siek Indiana University | ||
10:50 25mTalk | Robust Dynamic Embedding for Gradual Typing ICFP Papers Koen Jacobs Inria, Matías Toro University of Chile, Nicolas Tabareau Inria, Éric Tanter University of Chile DOI | ||
11:15 25mPaper | A simple blame calculus for explicit nulls JFP First Papers DOI | ||
11:40 25mTalk | SecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F* ICFP Papers Cezar-Constantin Andrici MPI-SP, Danel Ahman University of Ljubljana, Cătălin Hriţcu MPI-SP, Ruxandra Icleanu University of Edinburgh, Guido Martínez Microsoft Research, Exequiel Rivas Tallinn University of Technology; Ahrefs, Théo Winterhalter INRIA DOI | ||