SPLASH 2016 (series) / OOPSLA / Java and Scala's Type Systems are Unsound: The Existential Crisis of Null Pointers
Java and Scala's Type Systems are Unsound: The Existential Crisis of Null Pointers
We present short programs that demonstrate the unsoundness of Java and Scala's current type systems. In particular, these programs provide parametrically polymorphic functions that can turn any type into any type without (down)casting. Fortunately, parametric polymorphism was not integrated into the Java Virtual Machine (JVM), so these examples do not demonstrate any unsoundness of the JVM. Nonetheless, we discuss broader implications of these findings on the field of programming languages.
Conference DayFri 4 NovDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Conference Day
Fri 4 NovDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:10 | Typing, in PracticeOOPSLA at Matterhorn 1 Chair(s): Sebastian ErdwegDelft University of Technology, Netherlands | ||
10:30 25mTalk | A Practical Framework for Type Inference Error Explanation OOPSLA Calvin LoncaricUniversity of Washington, Satish ChandraSamsung Research America, Manu SridharanSamsung Research America, Cole SchlesingerSamsung Research America DOI Pre-print Media Attached | ||
10:55 25mTalk | Dynamically Diagnosing Type Errors in Unsafe Code OOPSLA Stephen KellUniversity of Cambridge DOI Media Attached | ||
11:20 25mTalk | First-Class Effect Reflection for Effect-Guided Programming OOPSLA DOI | ||
11:45 25mTalk | Java and Scala's Type Systems are Unsound: The Existential Crisis of Null Pointers OOPSLA Link to publication DOI Pre-print | ||