Supporting Unrestricted Recursive Types

Recursive types capture important invariants in programs and proofs. It is well-known that the naive treatment of unrestricted recursive types causes inconsistency. Typically, recursive types are admitted by putting various restrictions on their formations. This puts limitation and complexity on the usages of recursive types. In this paper we present a general approach to support unrestricted recursive types. Instead of putting restrictions on formation (introduction), we design the elimination rules to control the (dangerous) unfolding (elimination) of recursive types, while maintaining the intuition behind the naive understanding. Thus the usage of recursive types in our solution is simple and intuitive. Using System F as an example, we demonstrate how to safely admit recursive types and prove strong normalization for the new system. Our method is applicable to similar type systems and logics.