Bounded existentials and minimal typing
type: Item
instance of: scholarly article
title: Bounded existentials and minimal typing
zbMATH Open document ID: 0909.03017
DOI: 10.1016/S0304-3975(96)00300-3
author: G. Ghelli
author: Benjamin C. Pierce
published in: Theoretical Computer Science
publication date: 1998-08-13T00:00:00Z
review text: \(F_\leq\) is a typed lambda-calculus combining subtyping and second-order bounded quantification. It is shown that in the system obtained by adding (as primitive) bounded existential quantification the minimal type property fails. It is also shown that when the system is restricted to ``equal bounds'' (the introduction rules are of the form: If \(A\leq S\vdash T\leq U\) then \(\vdash\text{All } (A\leq S)T\leq\text{All } (A\leq S)U)\), then the minimal types do exist and an algorithm to get them is given.
Mathematics Subject Classification ID: 03B40
zbMATH DE Number: 1189762
zbMATH Keywords: typed lambda-calculus
zbMATH Keywords: subtyping
zbMATH Keywords: second-order bounded quantification
zbMATH Keywords: bounded existential quantification
zbMATH Keywords: minimal type property
MaRDI profile type: Publication
cites work: An extension of system \(F\) with subtyping
cites work: Coherence of subsumption, minimum typing and type-checking in F ≤
cites work: Q4281471
cites work: Divergence of \(F_{\leq}\) type checking
cites work: Bounded quantification is undecidable
description: scientific article; zbMATH DE number 1189762