Kevin Bierhoff
Kevin currently leads the Kotlin at Google team that brings Kotlin to Google's engineers. Kevin has also worked on supporting Java 8 in Android app development and other developer productivity projects.
Kevin holds a PhD from Carnegie Mellon University, where he worked on formalizing and enforcing API protocols. Since then, his research interests have included programming languages and how to help engineers write and maintain high-quality code.
Authored Publications
Google Publications
Other Publications
Sort By
Wildcards Need Witness Protection
Proceedings of the ACM on Programming Languages, vol. 6, 138:1-138:22 (to appear)
Preview abstract
In this paper, we show that the unsoundness discovered by Amin and Tate (2016) in Java’s wildcards is avoidable, even in the absence of a nullness-aware type system.
The key insight of this paper is that soundness in type systems that implicitly introduce existential types through subtyping hinges on still making sure there are suitable witness types when introducing existentially quantified type variables.
To show that this approach is viable, this paper formalizes a core calculus and proves it sound.
We used a static analysis based on our approach to look for potential issues in a vast corpus of Java code and found none (with 1 false positive).
This confirms both that Java's unsoundness has minimal practical consequence,
and that our approach can avoid it entirely with minimal false positives.
View details
No Results Found
