|
Liquid Intersection Types
Mário Pereira, Sandra Alves, Mário
Florido
Laboratório de Inteligência Artificial e Ciência de Computadores
R. Campo Alegre 687, 4169-007 Porto, Portugal
email: mariopereira@dcc.fc.up.pt,sandra@dcc.fc.up.pt,amf@dcc.fc.up.pt
April 2014
Abstract
We present a new type system combining refinement types and
the expressiveness of intersection type discipline. The use of such
features makes it possible to derive more precise types than in the
original refinement system. We have been able to prove several
interesting
properties for our system (including subject reduction) and developed
an inference algorithm, which we proved to be
sound.
|