ICFP 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025
Tue 14 Oct 2025 11:15 - 11:40 at Orchid Plenary Ballroom - Gradual Typing and Security Chair(s): Jeremy G. Siek

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 Oct

Displayed 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
25m
Talk
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
25m
Paper
A simple blame calculus for explicit nulls
JFP First Papers
Ondřej Lhoták University of Waterloo, Philip Wadler IOG; University of Edinburgh
DOI
11:40
25m
Talk
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