Labelled reductions, runtime errors, and operational subsumption

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, soft ware 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 ma y "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 fra mework 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 throu gh operational techniques, and furthermore provides an operational way to interpret recur sive type definitions.