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.
Fri 4 NovDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Fri 4 Nov
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:10 | Typing, in PracticeOOPSLA at Matterhorn 1 Chair(s): Sebastian Erdweg Delft University of Technology, Netherlands | ||
10:30 25mTalk | A Practical Framework for Type Inference Error Explanation OOPSLA Calvin Loncaric University of Washington, Satish Chandra Samsung Research America, Manu Sridharan Samsung Research America, Cole Schlesinger Samsung Research America DOI Pre-print Media Attached | ||
10:55 25mTalk | Dynamically Diagnosing Type Errors in Unsafe Code OOPSLA Stephen Kell University 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 | ||