Bounded existentials and minimal typing

We study an extension of the second-order calculus of bounded quantification, System F ⩽, with bounded existential types. Surprisingly, the most natural formulation of this extension lacks the important minimal typing property of F ⩽, which ensures that the set of types possessed by a typeable term can be characterized by a single least element. We consider alternative formulations and give an algorithm computing minimal types for the slightly weaker Kernel Fun variant of F ⩽.

Authors

• Giorgio Ghelli
• Benjamin Pierce

Keywords

No keywords are indexed for this paper.