Logo
LogoUniGeSES

ASG list of publications

Citation

Laurent Dami , "Labelled Reductions, Runtime Errors and Operational Subsumption", July, 1997

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-independent 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.

Bibtex

@unpublished{Dami97b,
Author = "Laurent Dami ",
Title = "Labelled Reductions, Runtime Errors and Operational Subsumption",
Key = "osg osg-ftp tr97.3 lambda-calculus",
Notes = "",
Month = "July",
Year = "1997"
}
Additional credits :
© 2004-2006 Bibliography Tool based on Marc Falcone's bachelor project.