Abstract
This paper discusses decidability and existence of principal types in type assignment systems for λ-terms in which types are considered modulo an equivalence relation induced by a set of type equations. There are two interesting ways of defining such equivalence, an initial and a final one. A suitable transformation will allow to treat both in an uniform way.
Chapter PDF
Similar content being viewed by others
Keywords
References
M. Brandt and F. Henglein. Coinductive axiomatization of recursive type equality and subtyping. In P. de Groote and J. R. Hindley, editors, Typed Lambda Calculi and Applications, volume 1210 of Lecture Notes in Computer Science, pages 63–81. Springer-Verlag, 1997.
V. Breazu-Tannen and A. Meyer. Lambda calculus with constrained types. In R. Parikh, editor, Logics of Programs, volume 193 of Lecture Notes in Computer Science, pages 23–40. Springer-Verlag, 1985.
F. Cardone and M. Coppo. Type inference with recursive types. Syntax and Semantics. Information and Computation, 92(1):48–80, 1991.
B. Courcelle. Fundamental properties of infinite trees. Theoretical Computer Science, 25:95–169, 1983.
J.R. Hindley. The principal type scheme of an object in combinatory logic. Transactions of the American Mathematical Society, 146:29–60, 1969.
J.W. Klop. Term rewriting systems. In Dov M. Gabbay S. Abramsky and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, pages 1–116. Oxford University Uress, New York, 1992.
M. Marz. An algebraic view on recursive types. Applied Categorical Structures, 7(12):147–157, 1999.
R. Milner. A Theory of Type Polimorphism in Programming. Journal of Computer and System Sciences, 17:348–375, 1978.
R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. MIT Press, 1990.
D. Scott. Some philosophical issues concerning theories of combinators. In C. Bohm, editor, Lambda calculus and computer science theory, volume 37 of Lecture Notes in Computer Science, pages 346–366. Springer-Verlag, 1975.
R. Statman. Recursive types and the subject reduction theorem. Technical Report 94-164, Carnegie Mellon University, 1994.
B. Pierce V. Gapeyev, M. Levin. Recursive subtyping revealed. In Proceedings fifth ACM SIGPLAN International Conference on Functional Programming, pages 221–232. ACM press, 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Coppo, M. (2001). Type Inference with Recursive Type Equations. In: Honsell, F., Miculan, M. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2001. Lecture Notes in Computer Science, vol 2030. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45315-6_12
Download citation
DOI: https://doi.org/10.1007/3-540-45315-6_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41864-1
Online ISBN: 978-3-540-45315-4
eBook Packages: Springer Book Archive