Logo
LogoUniGeSES

ASG list of publications

Citation

Laurent Dami, "Functions, Records and Compatibility in the Lambda N Calculus", in Object-Oriented Software Composition, pp. 153-174, , , , 1995

Abstract

Subtyping, a fundamental notion for software reusability, establishes a classification of data according to a compatibility relationship. This relationship is usually associated with records. However, compatibility can be defined in other situations, involving for example enumerated types or concrete data types. We argue that the basic requirement for supporting compatibility is an interaction protocol between software components using names instead of positions. Based on this principle, an extension of the lambda calculus is proposed, which combines de Bruijn indices with names. In the extended calculus various subtyping situations mentioned above can be modelled; in particular, records are encoded in a straightforward way. Compatibility is formally defined in terms of an operational lattice based on observation of error generation. Unlike many usual orderings, errors are not identified with divergence; as a matter of fact, both are even opposite since they respectively correspond to the bottom and top elements of the lattice. Finally, we briefly explore a second extension of the calculus, providing meet and join operators through a simple operational definition, and opening interesting perspectives for type checking and concurrency.

Bibtex

@inbook{Dami95a,
Author = "Laurent Dami",
Title = "Functions, Records and Compatibility in the Lambda N Calculus",
Booktitle = "Object-Oriented Software Composition",
Chapter = "",
Volume = "",
Publisher = "Prentice Hall",
Edition = "O. Nierstrasz and D. Tsichritzis",
Series = "",
ISBN = "",
Address = "",
Key = "olit osg OOSC06",
Notes = "",
Month = "",
Year = "1995"
}
Additional credits :
© 2004-2006 Bibliography Tool based on Marc Falcone's bachelor project.