Autori: Gavin M. Bierman, Andrew D. Gordon, Cătălin Hriţcu, David Langworthy

Editorial: ACM Press, 15th ACM SIGPLAN International Conference on Functional Programming (ICFP 2010), 2010.

Rezumat:

We study a first-order functional language with the novel combination of the ideas of refinement type (the subset of a type to satisfy a Boolean expression) and type-test (a Boolean expression testing whether a value belongs to a type). Our core calculus can express a rich variety of typing idioms; for example, intersection, union, negation, singleton, nullable, variant, and algebraic types are all derivable. We formulate a semantics in which expressions denote terms, and types are interpreted as first-order logic formulas. Subtyping is defined as valid implication between the semantics of types. The formulas are interpreted in a specific model that we axiomatize using standard first-order theories. On this basis, we present a novel type-checking algorithm able to eliminate many dynamic tests and to detect many errors statically. The key idea is to rely on an SMT solver to compute subtyping efficiently. Moreover, interpreting types as formulas allows us to call the SMT solver at run-time to compute instances of types.

Cuvinte cheie: procesarea datelor, satisfiabilitate modulo teorii, semantic subtyping, sisteme de tipuri // data processing, satisfiability modulo theories, semantic subtyping, type systems

URL: http://research.microsoft.com/en-us/projects/dminor/