Coppo, M. A completeness theorem for recursively defined types. (English) Zbl 0585.68047 Automata, languages and programming, 12th Colloq., Nafplion/Greece 1985, Lect. Notes Comput. Sci. 194, 120-129 (1985). Summary: [For the entire collection see Zbl 0563.00018.] In this paper the notion of recursively defined type for a functional language is studied. The semantics of types (which are interpreted as subsets of a type-free domain following R. Milner [J. Comput. Syst. Sci. 17, 348-375 (1978; Zbl 0388.68003)]) is built by successive approximations. Using the properties of our construction, an algorithm to decide semantic equality between (recursively defined) types is given. Moreover a system of formal rules to assign types to terms, which is complete with respect to the above semantics, is introduced. A recursive subsystem is complete for terms in normal form. Cited in 9 Documents MSC: 68Q65 Abstract data types; algebraic specification 68Q60 Specification and verification (program logics, model checking, etc.) 03B40 Combinatory logic and lambda calculus Keywords:functional language; semantics of types; type-free domain; algorithm to decide semantic equality Citations:Zbl 0563.00018; Zbl 0388.68003 PDF BibTeX XML OpenURL