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

• Type: Conference
• Year: 2006
• Where: POPL
• Authors: Cormac Flanagan
• Keywords: Hybrid Type Checking, Kinds Specificationsthey Support, POPL 2006, Programming Languages, Verification General Terms