Recu.rsive Types: the syntactic and semantic approaches

Abstract. The aim of this paper is to study some basic syntactic prop-erties of type inference systems with recursive types, and in particu-lar normalization, subject reduction and the existence of principal type schemes. We do not intend to present original results. Most of material presented here, except some results about the decidability of type infer-ence, has already been subject of some other papers (the main sources are [18], [12] and [5] $) $ or is part of the folklore of the subject. Our main contribution is to have put it in a uniform frame.