Publications:Gradual typing for objects

Jump to: navigation, search

Do not edit this section

Keep all hand-made modifications below

Title Gradual typing for objects
Author Jeremy Siek and Walid Taha
Year 2007
PublicationType Conference Paper
HostPublication ECOOP 2007 – Object-Oriented Programming : 21st European Conference, Berlin, Germany, July 30 - August 3, 2007. Proceedings
Conference 21st European Conference on Object-Oriented Programming (ECOOP 2007), Tech Univ Berlin, Berlin, GERMANY, JUL 30-AUG 03, 2007
Diva url
Abstract Static and dynamic type systems have well-known strengthsand weaknesses. In previous work we developed a gradual type system fora functional calculus named λ?→. Gradual typing provides the benefits ofboth static and dynamic checking in a single language by allowing theprogrammer to control whether a portion of the program is type checkedat compile-time or run-time by adding or removing type annotations onvariables. Several object-oriented scripting languages are preparing toadd static checking. To support that work this paper develops Ob?<:,a gradual type system for object-based languages, extending the Ob<:calculus of Abadi and Cardelli. Our primary contribution is to show thatgradual typing and subtyping are orthogonal and can be combined in aprincipled fashion. We also develop a small-step semantics, provide amachine-checked proof of type safety, and improve the space efficiencyof higher-order casts.