The Recursion Scheme from the Cofree Recursive Comonad

DOI10.1016/J.ENTCS.2011.02.020MaRDI QIDQ5166625zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Tarmo Uustalu, Varmo Vene

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

zbMATH Keywords

circular proofscofree comonadscofree recursive comonadscomonad-based recursionMendler recursionstructured recursion

Mathematics Subject Classification ID

Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15) Eilenberg-Moore and Kleisli constructions for monads (18C20) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Recursive coalgebras from comonads
• Recursive coalgebras from comonads
• Recursion schemes from comonads
• Cofree coalgebras and multivariable recursiveness.
• Recursive coalgebras of finitary functors
• scientific article; zbMATH DE number 5994844
• On well-founded and recursive coalgebras
• Categorical comprehensions and recursion
• scientific article; zbMATH DE number 4066868
• Combinational functors on co-r.e. structures

Cites work

• A natural extension of natural deduction
• Completely iterative algebras and completely iterative monads
• Completeness of Kozen's axiomatisation of the propositional \(\mu\)-calculus.
• Deforestation, program transformation, and cut-elimination
• Dinatural transformations
• Dualising initial algebras
• Generalised coinduction
• scientific article; zbMATH DE number 426302 (Why is no real title available?)
• scientific article; zbMATH DE number 431768 (Why is no real title available?)
• scientific article; zbMATH DE number 4210108 (Why is no real title available?)
• scientific article; zbMATH DE number 4047683 (Why is no real title available?)
• scientific article; zbMATH DE number 47007 (Why is no real title available?)
• scientific article; zbMATH DE number 1343506 (Why is no real title available?)
• scientific article; zbMATH DE number 1956528 (Why is no real title available?)
• scientific article; zbMATH DE number 2087442 (Why is no real title available?)
• Inductive types and type constraints in the second-order lambda calculus
• Infinite trees and completely iterative theories: A coalgebraic view
• Local model checking in the modal mu-calculus
• Programming Languages and Systems
• Recursion schemes from comonads
• Recursive coalgebras from comonads
• Recursive programming with proofs
• Tarski's fixed-point theorem and lambda calculi with monotone inductive types
• Termination checking with types
• Type-based termination of recursive definitions

Cited in

(5)

• Recursion schemes from comonads
• Conjugate hylomorphisms -- or: the mother of all structured recursion schemes
• Proof nets, coends and the Yoneda isomorphism
• Unifying structured recursion schemes. An extended study
• The Yoneda reduction of polymorphic types

This page was built for publication: The Recursion Scheme from the Cofree Recursive Comonad

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