Logical relations and inductive/coinductive types

Abstract

We investigate a λ calculus with positive inductive and coinductive types, which we call λ μ,ν, using logical relations. We show that parametric theories have the strong categorical properties, that the representable functors and natural transformations have the expected properties. Finally we apply the theory to show that terms of functorial type are almost canonical and that monotone inductive definitions can be reduced to positive in some cases.