Paper Info
Title
Products and polymorphic subtypes
Abstract
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 →, x 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 ⊢ 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 →, x, ∀ is undecidable, being already undecidable for the →, ∀ fragment (as proved in [15]), but for the x, ∀ fragment it turns out to be decidable.
Year
Venue
Keywords
2002
Fundam. Inform.
subtyping relation,logical system,complete hilbert style axiomatization,form e,typing assumption,polymorphic subtypes,logical semantics,cartesian product,polymorphic subtyping,gentzen style calculus,comprehensive study,sequent.,typing judgement,new form,natural deduction,sequent,binary tree,polymorphism
Field
DocType
Volume
Discrete mathematics,Combinatorics,Natural deduction,Cartesian product,Subject reduction,Binary tree,Decidability,Sequent,Subtyping,Mathematics,Undecidable problem
Journal
51
Issue
ISSN
Citations 
1
0169-2968
1
PageRank 
References 
Authors
0.36
12
2
Name
Order
Citations
PageRank
Viviana Bono129932.68
Jerzy Tiuryn21210126.00