Monotone (co)inductive types and positive fixed-point types
DOI10.1051/ITA:1999120zbMATH Open0940.03018OpenAlexW2059906894MaRDI QIDQ4943545FDOQ4943545
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
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
iterationSystem Fprimitive recursioncoiterationmonotone coinductive typemonotone inductive typemonotonicity witnessretract typesextensions of polymorphically typed lambda-calculusfixed-points of monotone operatorsprimitive corecursion
Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40) Abstract data types; algebraic specification (68Q65)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Parallel reductions in \(\lambda\)-calculus
- Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
Cited In (8)
- Title not available (Why is that?)
- Tarski's fixed-point theorem and lambda calculi with monotone inductive types
- Title not available (Why is that?)
- Title not available (Why is that?)
- Some Remarks on Type Systems for Course-of-value Recursion
- Partiality, Revisited
- Two extensions of System F with (co)iteration and primitive (co)recursion principles
- Iteration and coiteration schemes for higher-order and nested datatypes
Uses Software
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)
