This paper describes a reduction from the halting problem of Turing machines to subtype checking in Java. It follows that subtype checking in Java is undecidable, which answers a question posed by Kennedy and Pierce in 2007. It also follows that Java’s type checker can recognize any recursive language, which improves a result of Gill and Levy from 2016. The latter point is illustrated by a parser generator for fluent interfaces.
Wed 18 Jan
10:30 - 10:55 Talk | ||||||||||||||||||||||||||||||||||||||||||
10:55 - 11:20 Talk | Radu GrigoreUniversity of Kent | |||||||||||||||||||||||||||||||||||||||||
11:20 - 11:45 Talk | Cyrus OmarCarnegie Mellon University, Ian VoyseyCarnegie Mellon University, Michael HiltonOregon State University, USA, Jonathan AldrichCarnegie Mellon University, Matthew HammerUniversity of Colorado, Boulder | |||||||||||||||||||||||||||||||||||||||||
11:45 - 12:10 Talk | Karl CraryCarnegie Mellon University |