HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Hierarchies of decidable extensions of bounded quantification

Abstract : The system $F_\leq$, the well-known second-order polymorphic typed $\lambda$-calculus with subtyping and bounded universal type quantification [Cardelli-Wegner 85], [Bruce-Longo 90], [Curien-Ghelli 92], [Pierce 92], [Cardelli-Martini-Mitchell-Scedrov 94], appears to be undecidable [Pierce 92] because of undecidability of its subtyping component. Attempts were made to obtain decidable type systems with subtyping by weakening $F_\leq$ [Castagna-Pierce 94], [Katiyar-Sankar 92], and also by reinforcing or \em extending\/ it [Vorobyov 94]. However, for the moment, these extensions lack the important proof-theoretic minimum type property, which holds for $F_\leq$ and guarantees that each typable term has the minimum type, being a subtype of any other type of the term [Curien-Ghelli 92], [Vorobyov 94]. As a preparation step to introducing the extensions of $F_\leq$ with the minimum type property and the decidable term typing relation, we define and study here the hierarchies of decidable extensions of the$F_\leq$ subtyping relation. We demonstrate conditions providing that each theory in a hierarchy: \beginenumerate \item extends $F_\leq$, proving everything that is $F_\leq$-provable \item satisfies the substitution property for boundedly quantified universal types \item is transitive (transitivity and substitutivity are indispensable for the minimum type property and typing proof normalization). We give conditions guaranteeing that a hierarchy condenses and converges to $F_\leq$, and study cases when a hierarchy collapses.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 3:03:30 PM
Last modification on : Friday, February 4, 2022 - 3:22:12 AM
Long-term archiving on: : Monday, April 5, 2010 - 12:08:24 AM


  • HAL Id : inria-00074323, version 1



Sergei Vorobyov. Hierarchies of decidable extensions of bounded quantification. [Research Report] RR-2354, INRIA. 1994. ⟨inria-00074323⟩



Record views


Files downloads