Liquid Intersection Types

Mário Pereira
(University of Porto, Department of Computer Science & LIACC)
Sandra Alves
(University of Porto, Department of Computer Science & LIACC)
Mário Florido
(University of Porto, Department of Computer Science & LIACC)

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.

In Jakob Rehof: Proceedings Seventh Workshop on Intersection Types and Related Systems (ITRS 2014), Vienna, Austria, 18 July 2014, Electronic Proceedings in Theoretical Computer Science 177, pp. 24–42.
Published: 17th March 2015.

ArXived at: http://dx.doi.org/10.4204/EPTCS.177.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org