Technical Report: DCC-2014-04

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.