Monotone (co)inductive types and positive fixed-point types
Monotone (co)inductive types and positive fixed-point types
We study five extensions of the polymorphically typed lambda-calculus (system ) by type constructs intended to model fixed-points of monotone operators. Building on work by Geuvers concerning the relation between term rewrite systems for least pre-fixed-points and greatest post-fixed-points of positive type schemes (, non-nested positive inductive and coinductive types) and so-called retract types, we show that there are reduction-preserving embeddings even between systems of monotone (co)inductive...
Preface
Page 1