Abstract
The paper presents a static type checking algorithm for a language which allows to declare, and to pass as parameters, types, type constructors (parametric types) and polimorphic functions. A program written in this language is translated into an expression in a suitable formalism, and this expression is reduced to a normal form which can be either error or a type correct expression. This approach can also be described as that of giving a non-standard interpretation to programs (in this case a symbolic interpretation) using a denotational semantics technique.
Chapter PDF
References
Asirelli P., Gimona F., Martelli A., Montanari U. Passing parameter types in programming languages with data abstractions. AICA '77 Congress, Pisa, October 1977, 429–444.
Asirelli P., Martelli A., Montanari U. Language constructs for controlling side effects. Internal Report OL78-6, IEI, Pisa, December 1978, Submitted for publication.
Asirelli P., Degano P., Levi G., Martelli A., Montanari U., Pacini G., Sirovich F., Turini F. A flexible environment for program development based on a symbolic interpreter. Proc. Fourth Int. Conference on Software Engineering, Munich, September 1979, 251–263.
Barbuti R. Verifica dei tipi statica per un linguaggio con procedure polimorfe. AICA '79 Congress, Bari, October 1979.
Cousot P., Cousot R. Static determination of dynamic properties of generalized type unions. Language Design for Reliable Software, SIGPLAN Notices, 12, 3, March 1977, 77–94.
Demers A., Donahue J., Skinner G. Data types as values: Polimorphism, Type-checking, Encapsulation. Proc. Fifth ACM Symposium on Principles of Programming Languages, Tucson, January 1978, 23–30.
Donahue J. On the semantics of "Data types". SIAM J. Computing, 8, 4, November 1979, 546–560.
Donzeau-Gouge V. Utilization de la semantique denotationelle pour la description d'interpretations non-standard: application a la validation et a l'optimisation des programmes. Third International Symp. on Programming, Paris, March 1978, 315–335.
Ermine F., Ressouche A. Une methode de verification statique de types. Application au langage Pascal. Third International Symp. on Programming, Paris, March 1978, 292–314.
Henderson P. An approach to compile time type checking. Information Processing 77, North Holland 1977, 523–527.
Ichbiah J.D. et al. Rationale for the design of the ADA programming language. SIGPLAN Notices, 14, 7, July 1979.
Lampson B.W., Horning J.J., London R.L., Mitchell J.G., Popek G.L. Report on the programming language Euclid. SIGPLAN Notices (ACM) 12, 2, 1977.
Ledgard H.F. A model for type checking — with an application for Algol 60. Comm. ACM, 15, 11, November 1972, 956–966.
Milner R. A theory of type polymorphism in programming. J. Comp and System Sciences, 17, 1978, 348–375.
Mitchell J.G., Maybury W., Sweet R. Mesa language manual. Version 5.0. CSL-79-3, XEROX PARC, April 1979.
Solomon M. Type definition with parameters. Proc. Fifth ACM Symposium on Principles of Programming Languages, Tucson, January 1978, 31–37.
Reynolds J.C. Toward a theory of type structure. Lecture Notes in Comp. Science 19, Springer Verlag, Proc. Programming Symp., 1974, 408–425.
Tennent R.D. On a new approach to representation-independent data classes. Acta Inform., 1977, 315–324.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1980 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barbuti, R., Martelli, A. (1980). Static type checking for languages with parametric types and polymorphic procedures. In: Robinet, B. (eds) International Symposium on Programming. Programming 1980. Lecture Notes in Computer Science, vol 83. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-09981-6_1
Download citation
DOI: https://doi.org/10.1007/3-540-09981-6_1
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-09981-9
Online ISBN: 978-3-540-39233-0
eBook Packages: Springer Book Archive