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

Title: Typed Operational Semantics for Higher Order Subtyping

Speaker: Adriana Compagnoni

Abstract: 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.