Searching for just a few words should be enough to get started. If you need to make more complex queries, use the tips below to guide you.
Issue title: Concurrency Specification and Programming Workshop (CS&P'2001)
Article type: Research Article
Authors: Bono, Viviana | Tiuryn, Jerzy
Affiliations: Dipartimento di Informatica, Università di Torino, c. Svizzera 185, 10149 Torino, Italy | Institute of Informatics, Warsaw University, ul. Banacha 2, 02-097 Warsaw, Poland
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 →, × 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 →,×,∀ is undecidable, being already undecidable for the →,∀ fragment (as proved in [15]), but for the ×,∀ fragment it turns out to be decidable.
Keywords: Polymorphic Subtyping, Cartesian Product, Logical Semantics, Sequent
Journal: Fundamenta Informaticae, vol. 51, no. 1-2, pp. 13-41, 2002
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
USA
Tel: +1 703 830 6300
Fax: +1 703 830 2300
sales@iospress.com
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
IOS Press
Nieuwe Hemweg 6B
1013 BG Amsterdam
The Netherlands
Tel: +31 20 688 3355
Fax: +31 20 687 0091
info@iospress.nl
For editorial issues, permissions, book requests, submissions and proceedings, contact the Amsterdam office info@iospress.nl
Inspirees International (China Office)
Ciyunsi Beili 207(CapitaLand), Bld 1, 7-901
100025, Beijing
China
Free service line: 400 661 8717
Fax: +86 10 8446 7947
china@iospress.cn
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
如果您在出版方面需要帮助或有任何建, 件至: editorial@iospress.nl