Positive recursive type assignment

  • Pawel Urzyczyn
Contributed Papers Unification, Rewriting, Type Theory
Part of the Lecture Notes in Computer Science book series (LNCS, volume 969)


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.


Assignment System Regular Tree Positive System Type Inference Label Tree 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 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. 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. 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. 4.
    Cardone, F., Coppo, M., Type inference with recursive types: syntax and semantics, Information and Computation, 92 (1991), 48–80.Google Scholar
  5. 5.
    Klop, J.W., Combinatory Reduction Systems, Mathematisch Centrum, Amsterdam, 1980.Google Scholar
  6. 6.
    Marz, M., Private communication, 1994.Google Scholar
  7. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Pawel Urzyczyn
    • 1
  1. 1.Institute of InformaticsWarsaw UniversityWarsawPoland

Personalised recommendations