Abstract
A hierarchy of type assignment systems is defined, which is a complete stratification of the polymorphic type assignment system. For each of such systems a type inference algorithm is given.
Work partially supported by EEC "Project Stimulation ST2J/0374/C(EDB): Lambda Calcul Type".
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Barendregt, H.P., The Lambda Calculus: its Syntax and Semantics. North Holland, 1984 (revised version).
Ben-Yelles, C., Type Assignment in the Lambda-Calculus: Syntax and Semantics. Ph. D. Thesis, University College of Swansea, 1979.
Bosio, E., Ronchi Della Rocca, S., Type Synthesis for Intersection Type Discipline. Prooceedings of Third Italian Conference on Theoretical Computer Science. Word Scientific, 1989, pp.109–122.
Coppo, M., Tipi e polimorfismo nei linguaggi di programmazione, Atti degli Incontri di Logica Matematica, Siena, 1985.
Curry, H.B., Modified Basic Functionality in Combinatory Logic. Dialectica, 1969.
Damas, L. and Milner, R., The Principal Type Schemes for Functional Programs. In Symposium on Principles of Programming Languages, ACM, 1982, pp.207–212.
Giannini, P.,Honsell, F., Ronchi Della Rocca, S., A strongly normalizing term having no type in the system F (second order λ-calculus), Rapporto Interno, Dipartimento di Informatica, Torino, 1987.
Giannini, P., Ronchi Della Rocca, S., Characterization of typings in polymorphic type discipline. In Logic in Computer Science, IEEE, 1988, pp. 61–70.
Giannini, P., Ronchi Della Rocca, S., Message on the Type-Net, November 1989.
Girard, J.Y., Interpretation Fonctionelle et Elimination des Coupures de l'Arithmetique dOrdre Superieur. These D'Etat, Universite Paris VII, 1972.
Hindley, R., The Principal Type Scheme of an Object in Combinatory Logic. Transactions of American Mathematical Society, 1969, pp. 1–17.
Kfoury, A.J., Tiuryn J., Urzyczyn P., The Undecidability of Semiunification Problem. Tec. Report, Computer Science Dept., Boston University, 1989.
Le Chenadec P., On the Logic of Unification. Journal of Symbolic Computation, 8, 1/2, 1989, pp. 141–199.
Leivant, D., Polymorphic Type Inference. In Symposium on Principles of Programming Languages, ACM, 1983, pp.88–98.
Mitchell, J.C., Polymorphic Type Inference and Containment. Information and Computation 76, 2/3, 1988, pp.211–249.
Pfenning, F., Partial Polymorphic Type Inference and Higher-Order Unification. In Conference on LISP and Functional Programming, ACM, 1988.
Prawitz, D., Natural Deduction, a Proof Theoretic Study. Almquist and Wiksell, Amsterdam, 1965.
Reynolds, J.C., Towards a Theory of Type Structures. In Paris Colloquium on Programming, Springer Verlag, 1974, pp.408–425.
Robinson, J.A., A Machine Oriented Logic Based on the Resolution Principle. Journal of the ACM, 1965, pp.24–41.
Ronchi Della Rocca, S., Principal Type Scheme and Unification for Intersection Type Discipline. Theoretical Computer Science 59, 1988, pp.181–209.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Giannini, P., Ronchi, S., Rocca, D. (1991). Type inference in polymorphic type discipline. In: Ito, T., Meyer, A.R. (eds) Theoretical Aspects of Computer Software. TACS 1991. Lecture Notes in Computer Science, vol 526. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54415-1_39
Download citation
DOI: https://doi.org/10.1007/3-540-54415-1_39
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54415-9
Online ISBN: 978-3-540-47617-7
eBook Packages: Springer Book Archive