Monotone (co)inductive types and positive fixed-point types

DOI10.1051/ita:1999120zbMath0940.03018OpenAlexW2059906894MaRDI QIDQ4943545

Ralph Matthes

Publication date: 24 July 2000

Published in: RAIRO - Theoretical Informatics and Applications (Search for Journal in Brave)

Full work available at URL: https://eudml.org/doc/222026

zbMATH Keywords

iterationprimitive recursionSystem Fcoiterationmonotone coinductive typemonotone inductive typemonotonicity witnessretract typesextensions of polymorphically typed lambda-calculusfixed-points of monotone operatorsprimitive corecursion

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Related Items (3)

Some Remarks on Type Systems for Course-of-value Recursion ⋮ Iteration and coiteration schemes for higher-order and nested datatypes ⋮ Two extensions of system F with (co)iteration and primitive (co)recursion principles

Uses Software

• Automath

Cites Work

• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• Parallel reductions in \(\lambda\)-calculus
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Monotone (co)inductive types and positive fixed-point types