Positive recursive type assignment
- 930 Downloads
We consider several different definitions of type assignment with positive recursive types, from the point of view of their typing ability. We discuss the relationships between these systems. In particular, we show that the class of typable pure lambda terms remains the same for different type disciplines involving positive type fixpoints, and that type reconstruction is decidable.
KeywordsAssignment System Regular Tree Positive System Type Inference Label Tree
Unable to display preview. Download preview PDF.
- 1.Barendregt., H.P., Lambda Calculi with Types, Chapter 1 in: Handbook of Logic in Computer Science, vol 2, (S. Abramsky, Dov.M. Gabbay, and T.S.E. Maibaum, Eds.) Clarendon Press, 1992, pp. 118–310.Google Scholar
- 2.Breazu-Tannen, V., Meyer, A.R., Lambda calculus with constrained types, in: Logics of Programs (R. Parikh, Ed.), LNCS 193, Springer, Berlin, 1985.Google Scholar
- 3.Cardone, F., Coppo, M., Two extensions of Curry's type inference system, in: Logic and Computer Science (P. Oddifreddi, Ed.), Academic Press, 1990, pp. 19–75.Google Scholar
- 4.Cardone, F., Coppo, M., Type inference with recursive types: syntax and semantics, Information and Computation, 92 (1991), 48–80.Google Scholar
- 5.Klop, J.W., Combinatory Reduction Systems, Mathematisch Centrum, Amsterdam, 1980.Google Scholar
- 6.Marz, M., Private communication, 1994.Google Scholar
- 7.Mendler, N.P., Inductive types and type constraints in the second-order lambda calculus, Annals of Pure and Applied Logic, 51 (1991), 159–172.Google Scholar