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.

• Type: Conference
• Year: 1995
• Where: TLCA
• Authors: Healfdene Goguen
• Keywords: Object Oriented Programming, Theoretical Computer Science, TLCA 1995, Typed Operational Semantics, Wegner’s Kernel Fun