[Prev][Next][Index][Thread]

paper available





We would like to announce the availability of the following paper.


TITLE:    Typed Operational Semantics for Higher Order Subtyping
AUTHORS:  Adriana Compagnoni, Healfdene Goguen
ADDRESS:  
  Department of Computer Science, University of Edinburgh
  The King's Buildings, Edinburgh, EH9 3JZ, United Kingdom
ABSTRACT:
  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 variant of
  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.

It is available from ftp://ftp.dcs.ed.ac.uk/pub/abc/toshos.ps


Adriana Compagnoni and Healfdene Goguen