Typed Operational Semantics

9 years 1 months ago
Typed Operational Semantics
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ω ≤, a variant of 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ω ≤, using a Kripke model to prove soundness. The typed operational semantics provides a powerful tool to establish the metatheoretic properties of Fω ≤, such as Church–Rosser, subject reduction, the admissibility of structural rules, and the equivalence with the algorithmic presentation of the system.
Healfdene Goguen
Added 26 Aug 2010
Updated 26 Aug 2010
Type Conference
Year 1995
Where TLCA
Authors Healfdene Goguen
Comments (0)