Sciweavers

Share
APLAS
2007
ACM

Mixed Inductive/Coinductive Types and Strong Normalization

9 years 5 months ago
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.
Andreas Abel
Added 12 Aug 2010
Updated 12 Aug 2010
Type Conference
Year 2007
Where APLAS
Authors Andreas Abel
Comments (0)
books