Mixed inductive/coinductive types and strong normalization

Abstract

We introduce the concept of guarded saturated sets, saturated sets of strongly normalizing terms closed under folding of corecursive functions. Using this tool, we can model equi-inductive and equicoinductive types with terminating recursion and corecursion principles. Two type systems are presented: Mendler (co)iteration and sized types. As an application we show that we can directly represent the mixed inductive/coinductive type of stream processors with associated recursive operations. © Springer-Verlag Berlin Heidelberg 2007.