Java and Scala's Type Systems are Unsound: The Existential Crisis of Null Pointers
Amin, Nada; Tate, Ross
2015

Files

Abstract

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.

Details

Title Java and Scala's Type Systems are Unsound: The Existential Crisis of Null Pointers
Author(s) Amin, Nada ; Tate, Ross
Published in Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications
Conference OOPSLA 2016, Amsterdam, Netherlands, November 02 - 04, 2016
Date 2015
Keywords
DOI https://doi.org/10.1145/2983990.2984004
Laboratories LAMP
Record Appears in Scientific production and competences > I&C - School of Computer and Communication Sciences > IINFCOM > LAMP - Programming Methods Laboratory
Peer-reviewed publications
Conference Papers
Work produced at EPFL
Published
Record creation date 2017-03-31

PDF