Write a Blog >>
CC 2017
Sun 5 - Mon 6 February 2017 Austin, Texas, United States
Sun 5 Feb 2017 15:30 - 16:00 at 404 - Types

Object-oriented languages like Java and C# allow the <null> value for all references. This supports many flexible patterns, but has led to many errors, security vulnerabilities, and system crashes. % Static type systems can prevent null-pointer exceptions at compile time, but require annotations, in particular for used libraries. Conservative defaults choose the most restrictive typing, preventing many errors, but requiring a large annotation effort. Liberal defaults choose the most flexible typing, requiring less annotations, but giving weaker guarantees. Trusted annotations can be provided, but are not checked and require a large manual effort. None of these approaches provide a strong guarantee that the checked part of the program is isolated from the unchecked part: even with conservative defaults, null-pointer exceptions can occur in the checked part.

This paper presents \project, a gradual type system for null-safety. Developers start out verifying null-safety for the most important components of their applications. At the boundary to unchecked components, runtime checks are inserted by \project{} to guard the verified system from being polluted by unexpected <null> values. This ensures that null-pointer exceptions can only occur within the unchecked code or at the boundary to checked code; the checked code is free of null-pointer exceptions.

We present \project{} for Java, define the checked-unchecked boundary, and how runtime checks are generated. We evaluate our approach on real world software annotated for null-safety. We demonstrate the runtime checks, and acceptable compile-time and run-time performance impacts. \project{} enables combining a checked core with untrusted libraries in a safe manner, improving on the practicality of such a system.

Sun 5 Feb
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

15:30 - 16:30: Research Papers - Types at 404
CC-2017-papers15:30 - 16:00
Dan BrotherstonUniversity of Waterloo, Canada, Werner DietlUniversity of Waterloo, Canada, Ondřej LhotákUniversity of Waterloo, Canada
CC-2017-papers16:00 - 16:30
Rumyana NeykovaImperial College London, UK, Nobuko YoshidaImperial College London