Two extensions of system F with (co)iteration and primitive (co)recursion principles
DOI10.1051/ita/2009015zbMath1197.03013OpenAlexW2112269051MaRDI QIDQ3653093
Publication date: 18 December 2009
Published in: RAIRO - Theoretical Informatics and Applications (Search for Journal in Brave)
Full work available at URL: https://eudml.org/doc/92934
iterationcoalgebrasprimitive recursioncorecursionsaturated setsSystem Fdialgebrascoiterationmonotone coinductive typemonotone inductive typemonotonicity witness
Functional programming and lambda calculus (68N18) Abstract data types; algebraic specification (68Q65) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40)
Cites Work
- Comparing Hagino's categorical programming language and typed lambda- calculi
- Automatic synthesis of typed \(\Lambda\)-programs on term algebras
- Recursive programming with proofs
- Iteration and coiteration schemes for higher-order and nested datatypes
- Non-strictly positive fixed points for classical natural deduction
- Category theory and computer science. Manchester, UK, September 5--8, 1989. Proceedings
- Inductive types and type constraints in the second-order lambda calculus
- Type fixpoints
- Recursion Schemes for Dynamic Programming
- Categories for Types
- From Algebras and Coalgebras to Dialgebras
- Monotone (co)inductive types and positive fixed-point types
- Some Remarks on Type Systems for Course-of-value Recursion
- The under-appreciated unfold
- Least and greatest fixed points in intuitionistic natural deduction
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Two extensions of system F with (co)iteration and primitive (co)recursion principles