Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Learn about a simplified approach to gradual typing systems that handle null values through this 23-minute conference presentation from ICFP 2025. Explore how researchers Ondřej Lhoták and Philip Wadler developed a more orthogonal blame calculus that addresses the interaction between legacy programming languages (like Java) that permit null values at every type and modern languages (like Scala or Kotlin) that explicitly indicate which types allow nulls. Discover how their new calculus improves upon previous work by Nieto et al. (2020) through using just one constructor for function types and one for possibly nullable types, while providing a standard proof of the blame theorem. Understand how this approach enables embedding terms between legacy and newer languages even when they are open, rather than requiring closed terms. Examine the mechanized Coq proofs that validate all results presented in this research on gradual typing and null safety.
