Liquid Intersection Types
Programming Languages
2015-03-18 v1
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.
Cite
@article{arxiv.1503.04908,
title = {Liquid Intersection Types},
author = {Mário Pereira and Sandra Alves and Mário Florido},
journal= {arXiv preprint arXiv:1503.04908},
year = {2015}
}
Comments
In Proceedings ITRS 2014, arXiv:1503.04377