Personal tools
You are here: Home Events Abstract Archives 1997 Typed Operational Semantics for Higher Order Subtyping

Typed Operational Semantics for Higher Order Subtyping

Adriana Compagnoni LFCS Theory Seminar Room 2511, JCMB, King's Buildings 4pm, Tuesday 11th November 1997

Bounded operator abstraction is a language construct relevant to object-oriented programming languages and to ML2000, the successor to Standard ML. We introduce a variant system F-Omega-Sub 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 the original system, using a Kripke model to prove soundness. The typed operational semantics provides a powerful tool to establish the metatheoretic properties of the system, such as Church--Rosser, subject reduction, the admissibility of structural rules, and the equivalence with the algorithmic presentation of the system.

This is joint work with Healfdene Goguen, and it has been published as LFCS report ECS-LFCS-97-361.

Document Actions