Paper Info
Title
Gradual Typing for Objects
Abstract
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.
Year
DOI
Venue
2007
10.1007/978-3-540-73589-2_2
ECOOP
Keywords
Field
DocType
type safety,gradual typing,functional calculus,dynamic type system,gradual type system,previous work,type annotation,dynamic checking,ob calculus,static checking,object oriented,scripting language,higher order,type system,dynamic typing
Type system,Manifest typing,Functional calculus,Programming language,Computer science,Theoretical computer science,Subtyping,Type safety,Duck typing,Scripting language,Gradual typing
Conference
Volume
ISSN
ISBN
4609
0302-9743
3-540-73588-7
Citations 
PageRank 
References 
166
6.35
22
Authors
2
Search Limit
100166
Name
Order
Citations
PageRank
Jeremy G. Siek156345.96
Walid Taha2102070.41