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

Editorial: Cambridge University Press, Journal of Functional Programming, 1, p.31-105, 2012.

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 a Satisfiability Modulo Theories solver to
compute subtyping efficiently. Moreover, using a satisfiability modulo theories solver allows
us to show the uniqueness of normal forms for non-deterministic expressions, provide precise
counterexamples when type-checking fails, detect empty types, and compute instances of types
statically and at run-time.

Cuvinte cheie: type systems, data processing, refinement types, semantic subtyping

URL: http://www.infsec.cs.uni-saarland.de/~hritcu/publications/dminor-jfp2012.pdf