paper available

• To: types@cs.indiana.edu
• Subject: paper available
• From: Adriana Compagnoni <abc@dcs.ed.ac.uk>
• Date: Mon, 26 May 1997 14:33:00 +0100
• Cc: hhg@dcs.ed.ac.uk
• Delivery-Date: Mon, 26 May 1997 08:44:33 -0500
• Reply-to: abc@dcs.ed.ac.uk

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

• Prev: CFP: WORKSHOP ON PARALLELISM AND IMPLEMENTATION TECHNOLOGY FOR (CONSTRAINT) LOGIC PROGRAMMING LANGUAGES
• Next: ACM Worshop in Poland
• Index(es):
  • Main
  • Thread