Book chapter
Open access

Labelled Reductions, Runtime Errors, and Operational Subsumption

ContributorsDami, Laurent
Published inObjects at large = Objets en liberté, Editors Tsichritzis, Dionysios, p. 43-69
PublisherGenève : Centre universitaire d'informatique
Publication date1997

When combining modules it may be the case that the assembly is partially incorrect (error-prone), but nevertheless useful in some contexts. However usual type system will reject such assemblies as soon as they detect a potential error. We propose a more liberal approach: an error in a software configuration is tolerated as long as there are contexts which can use it without reaching the error; as a result, software reusability is improved. We introduce a general framework which defines in a language-independant way what it means to be "erroneous", and under which conditions a component may "subsume" another (i.e. replace it in any context). This new semantics, based on the observation of errors, is then applied to a comparison of various lambda-calculi, and shown to be close to the well known approximation semantics. An interesting application is to use the subsumption semantics for a simple term model interpretation of subtyping. The framework also proposes a language-independent specification of labelled reduction, which is used as a technical tool to syntactically characterize finite approximation. This generalizes the work of Mason, Smith and Talcott on getting denotational structures through operational techniques, and furthermore provides an operational way to interpret recursive type definitions.

Citation (ISO format)
DAMI, Laurent. Labelled Reductions, Runtime Errors, and Operational Subsumption. In: Objects at large = Objets en liberté. Genève : Centre universitaire d’informatique, 1997. p. 43–69.
Main files (1)
Book chapter (Published version)
  • PID : unige:155308

Technical informations

Creation10/11/2021 1:49:00 PM
First validation10/11/2021 1:49:00 PM
Update time03/16/2023 1:28:43 AM
Status update03/16/2023 1:28:43 AM
Last indexation01/17/2024 2:28:08 PM
All rights reserved by Archive ouverte UNIGE and the University of GenevaunigeBlack