Back to Search
Start Over
Typed-operational semantics for higher-order subtyping
- Source :
-
Information & Computation . Aug2003, Vol. 184 Issue 2, p242. 56p. - Publication Year :
- 2003
-
Abstract
- Bounded operator abstraction is a language construct relevant to object oriented programming languages and to ML2000, the successor to Standard ML. In this paper, we introduce <f>Fω&les;</f>, a variant of <f>F<:ω</f> with this feature and with Cardelli and Wegner’s kernel Fun rule for quantifiers. We define a typed-operational semantics with subtyping and prove that it is equivalent with <f>Fω&les;</f>, using logical relations to prove soundness. The typed-operational semantics provides a powerful and uniform technique to study metatheoretic properties of <f>Fω&les;</f>, such as Church–Rosser, subject reduction, the admissibility of structural rules, and the equivalence with the algorithmic presentation of the system that performs weak-head reductions.Furthermore, we can show decidability of subtyping using the typed-operational semantics and its equivalence with the usual presentation. Hence, this paper demonstrates for the first time that logical relations can be used to show decidability of subtyping. [Copyright &y& Elsevier]
- Subjects :
- *OBJECT-oriented programming
*COMPUTER programming
Subjects
Details
- Language :
- English
- ISSN :
- 08905401
- Volume :
- 184
- Issue :
- 2
- Database :
- Academic Search Index
- Journal :
- Information & Computation
- Publication Type :
- Academic Journal
- Accession number :
- 10117082
- Full Text :
- https://doi.org/10.1016/S0890-5401(03)00062-2