Liquid Intersection Types

TL;DR

This paper introduces a novel type system called Liquid Intersection Types that combines refinement types with intersection types to achieve more precise typings and prove important properties, supported by a sound inference algorithm.

Contribution

It presents a new type system integrating refinement and intersection types, along with proofs of key properties and a sound inference algorithm.

Findings

More precise types than traditional refinement systems

Proved subject reduction property for the system

Developed a sound type inference algorithm

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.