Abstract
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.
(Summary)
Full paper to appear in Mathematical Structures in Computer Science.
Preview
Unable to display preview. Download preview PDF.
References
V.Breazu-Tannen, T.Coquand, C.Gunter, A.Scedrov: Inheritance and explicit coercion, Proc. of the Fourth Annual Symposium on Logic in Computer Science, 1989.
K.B.Bruce, G.Longo: Modest models for inheritance and explicit polymorphism, Proc. of the Third Annual Symposium on Logic in Computer Science, 1988.
K.B.Bruce, A.R.Meyer, J,C.Mitchell: The semantics of second order lambda calculus, Information and Computation, 1989 (to appear).
L.Cardelli, J.Donahue, L.Glassman, M.Jordan, B.Kalsow, G.Nelson: Modula-3 report, Research Report n.31, DEC Systems Research Center, Sep. 1988.
L. Cardelli: A semantics of multiple inheritance, in Information and Computation 76, pp 138–164, 1988. (First appeared in Semantics of Data Types, G.Kahn, D.B.MacQueen and G.Plotkin Ed. Lecture Notes in Computer Science n.173, Springer-Verlag 1984.)
L. Cardelli, P. Wegner: On understanding types, data abstraction and polymorphism, Computing Surveys, Vol 17 n. 4, pp 471–522, December 1985.
P.-L.Curien, G.Ghelli: Coherence of subsumption, to appear.
O. Dahl, K. Nygaard: Simula, an Algol-based simulation language, Communications of the ACM, Vol 9, pp. 671–678, 1966.
J-Y.Girard: Une extension de l'interprétation de Gödel à l'analyse, et son application à l'élimination des coupures dans l'analyse et la théorie des types, Proceedings of the second Scandinavian logic symposium, J.E.Fenstad Ed. pp. 63–92, North-Holland, 1971.
J-Y.Girard: Interprétation fonctionelle et élimination des coupures dans l'arithmétique d'ordre supérieur, Thèse de doctorat d'état, University of Paris, 1972.
L.A.Jategaonkar, J.C.Mitchell: ML with extended pattern matching and subtypes, Proc. of the ACM Conference on Lisp and Functional Programming, pp.198–211, 1988.
G.Longo, E.Moggi: Constructive natural deduction and its ‘ω-set’ interpretation, Report CMU-CS-88-131, CMU, Dept. of Computer Science, 1988.
B.Meyer: Object-oriented software construction, Prentice Hall, 1988.
R. Milner: A theory of type polymorphism in programming, Journal of Computer and System Science 17, pp. 348–375, 1978.
J.C.Mitchell: Coercion and type inference, Proc. of the 11th ACM Symposium on Principles of Programming Languages, pp.175–185, 1984.
J.C.Mitchell: A type inference approach to reduction properties and semantics of polymorphic expressions, Proc. Symposium on Lisp and Functional Programming, pp.308–319, 1986. (Revised version to appear in Logic Foundations of Functional Programming, ed. G. Huet, Addison-Wesley, 1989.)
J.C.Mitchell: Type systems for programming languages, in Handbook of Theoretical Computer Science, ed. J. van Leeuwen et al. North Holland, 1990 (to appear).
A.Ohori, P.Buneman, V.Breazu-Tannen: Database programming in Machiavelli — a polymorphic languaage with static type inference, Report MS-CIS-88-103, University of Pennsylvania, Computer and Information Science Dept., 1988.
A. Ohori, P. Buneman: Type inference in a database programming language, Proc. of the ACM Conference on LISP and Functional Programming, pp.174–183, Snowbird, Utah, 1988.
D. Rémy: Typechecking records and variants in a natural extension of ML, Proc. of the 16th ACM Symposium on Principles of Programming Languages, pp.77–88, 1989.
J.C.Reynolds: Towards a theory of type structure, in Colloquium sur la programmation pp. 408–423, Springer-Verlag Lecture Notes in Computer Science, n.19, 1974.
C.Schaffert, T.Cooper, B.Bullis, M.Kilian, C.Wilpolt: An introduction to Trellis/Owl, Proc. OOPSLA'86.
B.Stroustrup: The C++ programming language, Addison-Wesley 1986.
M.Wand: Complete Type Inference for Simple Objects, Proc. of the Second Annual Symposium on Logic in Computer Science, June 1987, Cornell University.
M.Wand: Type inference for record concatenation and multiple inheritance, Proc. of the Fourth Annual Symposium on Logic in Computer Science, pp. 92–97, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cardelli, L., Mitchell, J.C. (1990). Operations on records. In: Main, M., Melton, A., Mislove, M., Schmidt, D. (eds) Mathematical Foundations of Programming Semantics. MFPS 1989. Lecture Notes in Computer Science, vol 442. Springer, New York, NY. https://doi.org/10.1007/BFb0040253
Download citation
DOI: https://doi.org/10.1007/BFb0040253
Published:
Publisher Name: Springer, New York, NY
Print ISBN: 978-0-387-97375-3
Online ISBN: 978-0-387-34808-7
eBook Packages: Springer Book Archive