The Recursion Scheme from the Cofree Recursive Comonad
DOI10.1016/j.entcs.2011.02.020zbMath1291.68149OpenAlexW2110979194WikidataQ62043258 ScholiaQ62043258MaRDI QIDQ5166625
Publication date: 27 June 2014
Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.entcs.2011.02.020
structured recursioncircular proofscofree comonadscofree recursive comonadscomonad-based recursionMendler recursion
Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15) Eilenberg-Moore and Kleisli constructions for monads (18C20)
Related Items (2)
Cites Work
- Local model checking in the modal mu-calculus
- Recursive programming with proofs
- Infinite trees and completely iterative theories: A coalgebraic view
- Completely iterative algebras and completely iterative monads
- Completeness of Kozen's axiomatisation of the propositional \(\mu\)-calculus.
- Tarski's fixed-point theorem and lambda calculi with monotone inductive types
- Recursive coalgebras from comonads
- Inductive types and type constraints in the second-order lambda calculus
- A natural extension of natural deduction
- Generalised coinduction
- Dualising initial algebras
- Type-based termination of recursive definitions
- Termination checking with types
- Deforestation, program transformation, and cut-elimination
- Programming Languages and Systems
- Dinatural transformations
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: The Recursion Scheme from the Cofree Recursive Comonad
