[TYPES] System F omega with (equi-)recursive types

[Florian Lorenzen]

Dear types forum members,

I have been looking for publications studying the properties (type
safety, decidability of type checking, type checking algorithm) of
System F omega combined with (equi-)recursive types but have,
unfortunately, been quite unsuccessful. I am interested in an extension
of F omega where the X in (mu X. T) ranges over proper types of kind *.

I would very much appreciate any pointers into the literature.

Thank you and best regards,

Florian

-- 
Florian Lorenzen

Technische Universität Berlin
Fakultät IV - Elektrotechnik und Informatik
Übersetzerbau und Programmiersprachen

Sekr. TEL12-2, Ernst-Reuter-Platz 7, D-10587 Berlin

Tel.:   +49 (30) 314-24618
E-Mail: florian.lorenzen at tu-berlin.de
WWW:    http://www.user.tu-berlin.de/florenz