Inscriere cercetatori

Premii Ad Astra

premii Ad Astra

Asociația Ad Astra a anunțat câștigătorii Premiilor Ad Astra 2022: http://premii.ad-astra.ro/. Proiectul și-a propus identificarea și popularizarea modelelor de succes, a rezultatelor excepționale ale cercetătorilor români din țară și din afara ei.

Asociatia Ad Astra a cercetatorilor romani lanseaza BAZA DE DATE A CERCETATORILOR ROMANI DIN DIASPORA. Scopul acestei baze de date este aceea de a stimula colaborarea dintre cercetatorii romani de peste hotare dar si cu cercetatorii din Romania. Cercetatorii care doresc sa fie nominalizati in aceasta baza de date sunt rugati sa trimita un email la cristian.presura@gmail.com

Semantic Subtyping with an SMT Solver

Domenii publicaţii > Ştiinţe informatice + Tipuri publicaţii > Articol în revistã ştiinţificã

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