Mathematical Structures in Computer Science

Research Article

Operations on records

Luca Cardellia1 and John C. Mitchella2

a1 Digital Equipment Corporation, Systems Research Center, USA

a2 Department of Computer Science, Stanford University, USA


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.

(Received December 23 1989)

(Revised September 10 1990)