# Browse wiki

Jump to: navigation, search
Abstract

Static and dynamic type systems h …

Static and dynamic type systems have well-known strengths and weaknesses. In previous work we developed a gradual type system for a functional calculus named $\lambda^?_\to$. Gradual typing provides the benefits of both static and dynamic checking in a single language by allowing the programmer to control whether a portion of the program is type checked at compile-time or run-time by adding or removing type annotations on variables. Several object-oriented scripting languages are preparing to add static checking. To support that work this paper develops $\mathbf{Ob}^{?}_{<:}$, a gradual type system for object-based languages, extending the Ob < : calculus of Abadi and Cardelli. Our primary contribution is to show that gradual typing and subtyping are orthogonal and can be combined in a principled fashion. We also develop a small-step semantics, provide a machine-checked proof of type safety, and improve the space efficiency of higher-order casts.

fficiency of higher-order casts.

, 21st European Conference on Object-Oriented Programming, ECOOP 2007, Berlin, Germany, 30 July-3 August http://dx.doi.org/10.1007/978-3-540-73589-2_2  + http://hh.diva-portal.org/smash/record.jsf?searchId=1&pid=diva2:588266 27  + Conference Paper  + Springer  + Lecture Notes in Computer Science ; 4609  + 2  + Gradual Typing for Functional Languages  + 2007  + , , , , , , , , , 26 June 2014 03:45:00  +
 No properties link to this page.

Enter the name of the page to start browsing from.