Typed Operational Semantics for Higher Order Subtyping

Adriana Compagnoni and Healfdene Goguen


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 a language with this feature and with Cardelli and Wegner's kernel Fun rule for quantifiers. We define a typed operational semantics with subtyping and prove an equivalence result, using a Kripke model to prove soundness. The typed operational semantics provides a powerful tool to establish metatheoretic properties such as Church-Rosser, subject reduction, the admissibility of structural rules, and the equivalence with the algorithmic presentation of the system.


This report is available in the following formats:

Previous | Index | Next