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.

• Type: Conference
• Year: 2007
• Where: APLAS
• Authors: Andreas Abel
• Keywords: APLAS 2007, Associated Recursive Operations, Mixed Inductive/coinductive Type, Programming Languages, Strongly Normalizing