We define a simple collection of operations for creating and manipulating record structures, where records are intended as finite associations of values to labels. A second-order type system over these operations supports both subtyping and polymorphism. We provide typechecking algorithms and limited semantic models. Our approach unifies and extends previous notions of records, bounded quantification, record extension, and parametrization by row-variables. The general aim is to provide foundations for concepts found in object-oriented languages, within a framework based on typed lambda-calculus. Appears in: Theoretical Aspects of Object-Oriente Programming, C.Gunter, J.C.Mitchell Eds. MIT Press, 1994. Appears in: Mathematical Structures in Computer Science, vol 1, pp. 3-48, 1991 SRC Research Report 48, August 25, 1989. Revised October 22, 1993. © Digital Equipment Corporation 1989,1993. This work may not be copied or reproduced in whole or in part for any commercial purpose. Permissi...
Luca Cardelli, John C. Mitchell