Products and Polymorphic Subtypes

• Autorzy: Bono V. , Tiuryn J.
• Języki publikacji: EN

Abstrakty

EN

This paper is devoted to a comprehensive study of polymorphic subtypes with products. We first present a sound and complete Hilbert style axiomatization of the relation of being a subtype in presence of ->, × type constructors and the " quantifier, and we show that such axiomatization is not encodable in the system with ->," only. In order to give a logical semantics to such a subtyping relation, we propose a new form of a sequent which plays a key role in a natural deduction and a Gentzen style calculi. Interestingly enough, the sequent must have the form E\vdash T, where E is a non-commutative, non-empty sequence of typing assumptions and T is a finite binary tree of typing judgements, each of them behaving like a pushdown store. We study basic metamathematical properties of the two logical systems, such as subject reduction and cut elimination. Some decidability/undecidability issues related to the presented subtyping relation are also explored: as expected, the subtyping over ->,×," is undecidable, being already undecidable for the ->," fragment (as proved in [15]), but for the ×," fragment it turns out to be decidable.

Słowa kluczowe

EN

polymorphic subtyping; Cartesian product; logical semantics; sequent

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2002
• Tom: Vol. 51, nr 1,2
• Strony: 13--41
• Opis fizyczny: bibliogr. 15 poz.

Twórcy

autor

Bono V.

autor

Tiuryn J.

• Dipartimento di Informatica, Universita di Torino, c.Svizzera 185, 10149 Torino, Italy,