Semantic subtyping with an SMT solver

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

Research output: Contribution to journalArticlepeer-review

Abstract

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.
Original languageEnglish
Pages (from-to)31-105
Number of pages75
JournalJournal of Functional Programming
Volume22
Issue number1
DOIs
Publication statusPublished - 2012

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

Cite this