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

DOI10.1051/ITA:1999120MaRDI QIDQ4943545zbMATH OpenOpenAlexFDO

Authors 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, https://semanticscholar.org/paper/526b3a7806d8c6c49602aad71714ed512166a83a

zbMATH Keywords

iterationSystem Fprimitive recursioncoiterationmonotone coinductive typemonotone inductive typemonotonicity witnessretract typesextensions of polymorphically typed lambda-calculusfixed-points of monotone operatorsprimitive corecursion

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1342219
• Tarski's fixed-point theorem and lambda calculi with monotone inductive types
• scientific article; zbMATH DE number 18908
• A TYPE-FREE THEORY OF HALF-MONOTONE INDUCTIVE DEFINITIONS
• Monotonicity reasoning in formal semantics based on modern type theories
• scientific article; zbMATH DE number 3285192
• Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types
• Publication:4945244
• Type-theoretic interpretation of iterated, strictly positive inductive definitions

Cites work

• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 3485174 (Why is no real title available?)
• scientific article; zbMATH DE number 1342219 (Why is no real title available?)
• scientific article; zbMATH DE number 1342222 (Why is no real title available?)
• scientific article; zbMATH DE number 1385477 (Why is no real title available?)
• Parallel reductions in \(\lambda\)-calculus
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)

Cited in

(10)

• Type fixpoints, iteration vs. recursion
• scientific article; zbMATH DE number 1841846 (Why is no real title available?)
• scientific article; zbMATH DE number 2003163 (Why is no real title available?)
• Some remarks on type systems for course-of-value recursion
• Tarski's fixed-point theorem and lambda calculi with monotone inductive types
• Two extensions of System F with (co)iteration and primitive (co)recursion principles
• scientific article; zbMATH DE number 1385477 (Why is no real title available?)
• Partiality, Revisited
• Iteration and coiteration schemes for higher-order and nested datatypes
• Monotone recursive types and recursive data representations in Cedille

Describes a project that uses

Uses Software

• Automath

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4943545)