Hostname: page-component-78c5997874-v9fdk Total loading time: 0 Render date: 2024-11-16T19:18:25.712Z Has data issue: false hasContentIssue false
  • English
  • Français

Operations on records

Published online by Cambridge University Press:  04 March 2009

Luca Cardelli  and
John C. Mitchell
Luca Cardelli
Affiliation:
Digital Equipment Corporation, Systems Research Center, USA
John C. Mitchell
Affiliation:
Department of Computer Science, Stanford University, USA
Get access Rights & Permissions [Opens in a new window]

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.

Type
Research Article
Information
Mathematical Structures in Computer Science , Volume 1 , Issue 1 , March 1991 , pp. 3 - 48
Copyright
Copyright © Cambridge University Press 1991

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Breazu-Tannen, V., Coquand, T., Gunter, C. and Scedrov, A. (1989) Inheritance and explicit coercion. Proc. Fourth IEEE Symp. on Logic in Computer Science, pp. 112–129Google Scholar
Bruce, K.B. and Longo, G. (1988) A modest model of records, inheritance and bounded quantification. Proc. Third IEEE Symp. on Logic in Computer Science, pp. 38–50Google Scholar
Bruce, K.B., Meyer, A.R. and Mitchell, J.C. (1990) The semantics of second order lambda calculus. Informat. Computat. Vol. 85, No. 1, pp. 76–134CrossRefGoogle Scholar
Cardelli, L. (1988) A semantics of multiple inheritance. In Information and Computation 76 138–164 (First appeared in Semantics of Data Types, eds G. Kahn, D. B. MacQueen and G. Plotkin. Springer Lecture Notes in Computer Science 173, Springer-Verlag, 1984.)Google Scholar
Cardelli, L., Donahue, J., Glassman, L., Jordan, M., Kalsow, B. and Nelson, G. (1989) Modula-3 report (revised). Research Report no. 52, DEC Systems Research Center.Google Scholar
Cardelli, L. and Wegner, P. (1985) On understanding types, data abstraction and polymorphism. Comput. Surv. 17(4) 471–522Google Scholar
Curien, P.-L. and Ghelli, G. (1991) Coherence of subsumption. Math. Struct. Comp. Sci, to appear.CrossRefGoogle Scholar
Dahl, O. and Nygaard, K. (1966) Simula, an Algol-based simulation language. Commun. ACM 9 671–678CrossRefGoogle Scholar
Girard, J.-Y. (1971) Une extension de Interpretation de Gödel é l’analyse, et son application à l’élimination des coupures dans l’analyse ct la théorie des types. Proc. Second Scandinavian Logic Symposium, ed. Fenstad, J.E.. North-Holland, pp. 63–92Google Scholar
Girard, J.-Y. (1972) Interprétation fonctionelle et élimination des coupures dans 1’arithmétique d’ordre supérieur. Thèse de doctorat d’état, University of Paris.Google Scholar
Jategaonkar, L.A. and Mitchell, J.C. (1988) ML with extended pattern matching and subtypes. Proc. ACM Conf. on Lisp and Functional Programming, pp. 198–211Google Scholar
Longo, G. and Moggi, E. (1988) Constructive natural deduction and its ‘w-set’ interpretation. Report CMU-CS-88–131, CMU, Dept. of Computer Science, Math. Struct. Comput. Set. 1 (2) to appear.Google Scholar
Meyer, B. (1988) Object-oriented Software Construction. Prentice-Hall.Google Scholar
Milner, R. (1978) A theory of type polymorphism in programming. J. Comput. Sys. Sci. 17 348–375CrossRefGoogle Scholar
Mitchell, J.C. (1984) Coercion and type inference. Proc. 11th ACM Symp. on Principles of Programming Languages, pp. 175–185CrossRefGoogle Scholar
Mitchell, J.C. (1986) A type inference approach to reduction properties and semantics of polymorphic expressions. Proc. Symp. on Lisp and Functional Programming, pp. 308–319 (Revised version in Logic Foundations of Functional Programming, ed. G. Huet, Addison-Wesley, 1989, pp. 195–212)Google Scholar
Mitchell, J.C. (1990) Type systems for programming languages. In: Handbook of Theoretical Computer Science, Volume B, eds Leeuwen, J. vanet al., North-Holland, pp. 365–458Google Scholar
Ohori, A., Buneman, P. and Breazu-Tannen, V. (1988) database programming in Machiavelli – a polymorphic language with static type inference. Report MS-CIS-88–103, University of Pennsylvania, Computer and Information Science Department.Google Scholar
Ohori, A. and Buneman, P. (1988) Type inference in a Database programming language. Proc. ACM Conf on LISP and Functional Programming, pp. 174–183Google Scholar
Rémy, D. (1989) Typechecking records and variants in a natural extension of ML. Proc. 16th ACM Symp. on Principles of Programming Languages, pp. 77–88Google Scholar
Reynolds, J.C. (1974) Towards a theory of type structure. In: Colloquium sur la Programmation. Springer Lecture Notes in Computer Science 19, pp. 408–423Google Scholar
Schaffert, C., Cooper, T., Bullis, B., Kilian, M. and Wilpolt, C. (1986) An introduction to Trellis/Owl. Proc. ACM Conf. Object-Oriented Programming Systems, Languages and Applications, pp. 9–16Google Scholar
Stroustrup, B. (1986) The C++ Programming Language. Addison-Wesley.Google Scholar
Wand, M. (1987) Complete type inference for simple objects. Proc. Second IEEE Symp. on Logic in Computer Science, pp. 37–44Google Scholar
Wand, M. (1989) Type inference for record concatenation and multiple inheritance. Proc. Fourth IEEE Symp. on Logic in Computer Science, pp. 92–97Google Scholar