Book chapter
OA Policy
English

Labelled Reductions, Runtime Errors, and Operational Subsumption

ContributorsDami, Laurent
Published inTsichritzis, Dionysios (Ed.), Objects at large = Objets en liberté, p. 43-69
PublisherGenève : Centre universitaire d'informatique
Publication date1997
Abstract

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é. Tsichritzis, Dionysios (Ed.). Genève : Centre universitaire d’informatique, 1997. p. 43–69. doi: 10.1007/3-540-63165-8_231
Main files (1)
Book chapter (Published version)
accessLevelPublic
Identifiers
159views
77downloads

Technical informations

Creation11/10/2021 13:49:00
First validation11/10/2021 13:49:00
Update time06/01/2026 13:38:00
Status update06/01/2026 13:38:00
Last indexation06/01/2026 13:42:22
All rights reserved by Archive ouverte UNIGE and the University of GenevaunigeBlack