Inscriere cercetatori

Site nou !

Daca nu va puteti recupera parola (sau aveti alte probleme), scrieti-ne la pagina de contact. Situl vechi se gaseste la adresa


Semantic Subtyping with an SMT Solver

Domenii publicaţii > Ştiinţe informatice + Tipuri publicaţii > Articol în volumul unei conferinţe

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.


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