Strong normalization and equi-(Co)inductive types

Abstract

A type system for the lambda-calculus enriched with recursive and corecursive functions over equi-inductive and -coinductive types is presented in which all well-typed programs are strongly normalizing. The choice of equi-inductive types, instead of the more common isoinductive types, influences both reduction rules and the strong normalization proof. By embedding iso- into equi-types, the latter ones are recognized as more fundamental. A model based on orthogonality is constructed where a semantical type corresponds to a set of observations, and soundness of the type system is proven. © Springer-Verlag Berlin Heidelberg 2007.