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 F) 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 (i.e., 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...
Multilinearity of sketches.
Multiopérateurs - Multiopérations