2015/03/17 by Mário Pereira, Sandra Alves, Mário Florido
Computer Science · #cs.PL
paper · pdf · doi:10.4204/eptcs.177.3
published as EPTCS 177, 2015, pp. 24-42 · In Proceedings ITRS 2014, arXiv:1503.04377
arxiv created 2015/03/17 · arxiv updated 2015/03/18
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.