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

[Frederic Blanqui]

For termination, you may have a look at:

Strong Normalization and Equi-(co)inductive Types 
<http://www2.tcs.ifi.lmu.de/%7Eabel/tlca07.pdf> Andreas Abel
/Typed Lambda Calculi and Application, TLCA'07.

Best regards, Frederic.
/
Le 07/06/2011 00:07, Florian Lorenzen a écrit :
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
>
>
> 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
>