Cyclic Types

[Tobias . Nipkow]

PS If anyone wonders how to describe cyclic types in a linear fashion: you
introduce a type-var binding operator $\mu$ such that $\mu a.t$ represents
the solution to $a = t$, where $t$ may contain $a$. Then every closed
constant free term has type $\mu a.a \to a$.

Tobias