Hybrid type checking

11 years 6 months ago
Hybrid type checking
Traditional static type systems are very effective for verifying basic interface specifications, but are somewhat limited in the kinds specificationsthey support. Dynamically-checkedcontracts can enforce more precise specifications, but these are not checked until run time, resulting in incomplete detection of defects. Hybrid type checking is a synthesis of these two approaches that enforces precise interface specifications, via static analysis where possible, but also via dynamic checks where necessary. This paper explores the key ideas and implications of hybrid type checking, in the context of the simply-typed -calculus with arbitrary refinements of base types. Categories and Subject Descriptors D.3.1 [Programming Languages: Formal Definitions and Theory]: specification and verification General Terms Languages, Theory, Verification Keywords Type systems, contracts, static checking, dynamic checking
Cormac Flanagan
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2006
Where POPL
Authors Cormac Flanagan
Comments (0)