Semantic subtyping with an SMT solver

Gavin M. Bierman, Andrew D. Gordon, Catalin Hritcu, David E. Langworthy

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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.
Original languageEnglish
Title of host publicationProceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010
PublisherACM
Pages105-116
Number of pages12
ISBN (Print)978-1-60558-794-3
DOIs
Publication statusPublished - 2010

Fingerprint

Dive into the research topics of 'Semantic subtyping with an SMT solver'. Together they form a unique fingerprint.

Cite this