We study an extension of the second-order calculus of bounded quantification, System F-less than or equal to, with bounded existential types. Surprisingly, the most natural formulation of this extension lacks the important minimal typing property of F-less than or equal to, 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-less than or equal to.
|Autori:||GHELLI G; PIERCE B.|
|Titolo:||Bounded Existentials and Minimal Typing|
|Anno del prodotto:||1998|
|Digital Object Identifier (DOI):||10.1016/S0304-3975(96)00300-3|
|Appare nelle tipologie:||1.1 Articolo in rivista|