Wyniki wyszukiwania - BazTech

1

Big-step Operational Semantics Revisited

Dominik J., Kuśmierek M., Bono V.

Fundamenta Informaticae

|

2010

|

Vol. 103, nr 1-4

137-172

EN

In this paper we present a novel approach to big-step operational semantics. This approach stems from the observation that the typical type soundness property formulated via a big-step operational semantics is weak, while the option of using a small-step operational semantics is not always an option, because it is less intuitive to build and understand. We support our claim by using a simple language called LM, for which we present a big-step semantics expressed with the new approach, allowing one to formulate a stronger type soundness property. We prove this property for LM and we present an example of an error in the typing rules which does not violate the typical type soundness property, but does violate ours.

2

Products and Polymorphic Subtypes

Bono V., Tiuryn J.

Fundamenta Informaticae

|

2002

|

Vol. 51, nr 1,2

13-41

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.

3

A subtyping for extensible, incomplete objects

Bono V., Bugliesi M., Dezani-Ciancaglini M., Liquori L.

Fundamenta Informaticae

|

1999

|

Vol. 38, Nr 4

325-364

EN

We extend the type system for the Lambda Calculus of Objects with a mechanism of width subtyping and a treatment of incomplete objects. The main novelties over previous work are the use of subtype-bounded quantification to capture a new and more direct rendering of MyType polymorphism, and a uniform treatment for other features that were accounted for via different systems in subsequent extensions. The new system provides for (i) appropriate type specialization of inherited methods, (ii) static detection of errors, (iii) width subtyping compatible with object extension, and (iv) sound typing for partially specified objects.