Coalgebraic Non-Wellfounded Proofs: Recursiveness and GTC

Mayuko Kori

arxiv: 2605.15664 · v1 · pith:QYFIF5VUnew · submitted 2026-05-15 · 💻 cs.LO

Coalgebraic Non-Wellfounded Proofs: Recursiveness and GTC

Mayuko Kori This is my paper

Pith reviewed 2026-05-19 19:33 UTC · model grok-4.3

classification 💻 cs.LO

keywords non-wellfounded proofscoalgebrasglobal trace conditionrecursive coalgebrassoundnessmodal mu-calculusfixed-point logics

0 comments

The pith

Non-wellfounded proofs satisfy the global trace condition exactly when a related coalgebra is recursive, which ensures soundness through a unique semantic morphism.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces a coalgebraic approach to non-wellfounded proof systems where infinite derivation trees are represented as coalgebras. It shows that the global trace condition, which prevents invalid infinite paths, can be captured by the recursiveness of the coalgebra after applying an adjoint. This characterization allows soundness to be proved by establishing the existence of a unique morphism from the coalgebra to the semantic algebra. The framework is applied to examples including the modal mu-calculus and higher-order fixed-point logics, demonstrating how infinite proofs can be given rigorous meaning.

Core claim

In this coalgebraic framework, derivation trees are coalgebras of generalised polynomial functors on presheaves, and the global trace condition is formulated as a condition on graphs of coalgebras. The central result is that a coalgebra satisfies the GTC if and only if its image under a suitable adjoint is recursive. Given an appropriate assumption on the semantic algebra, this yields that every proof has a unique coalgebra-to-algebra morphism, which establishes soundness.

What carries the argument

Graphs of coalgebras for modelling derivation trees and the reduction of the global trace condition to the recursiveness of the adjoint image of the coalgebra.

If this is right

The modal mu-calculus has a sound non-wellfounded proof system under this model.
Higher-order fixed-point logics admit similar coalgebraic soundness proofs.
Circular proofs in mu-bicomplete categories can be handled via the same recursive coalgebra condition.
Soundness reduces to checking a local recursiveness property instead of global path conditions.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

This method could simplify checking validity in infinite proof systems by reducing global conditions to algebraic properties.
It may extend to other areas of logic that use circular or infinite reasoning.
Future work might explore algorithmic ways to verify the recursiveness in concrete systems.

Load-bearing premise

There is an assumption on the semantic algebra that guarantees a unique coalgebra-to-algebra morphism when the coalgebra is recursive.

What would settle it

A counterexample derivation in one of the example systems where the global trace condition holds but no unique morphism exists, or where recursiveness fails despite the condition being satisfied.

read the original abstract

Non-wellfounded proof systems impose a global condition called the global trace condition (GTC) on a derivation tree to ensure soundness. Providing a categorical characterisation of the GTC that guarantees soundness remains challenging due to the global, non-compositional nature of these conditions and the infinitary structure of non-wellfounded proofs. We develop a coalgebraic framework for non-wellfounded proof systems where derivation trees are modelled as coalgebras of generalised polynomial functors on presheaves. Since the GTC is a constraint on infinite paths in derivation graphs, we employ graphs of coalgebras and formulate the GTC coalgebraically as a condition on these graphs. Soundness is then formulated as the existence of a unique coalgebra-to-algebra morphism from a coalgebra representing a derivation graph to an algebra specifying semantics. Within this framework, we characterise the GTC via recursive coalgebras: a coalgebra satisfies the GTC if and only if its image under a suitable adjoint is recursive. Under an appropriate assumption on the given semantic algebra, this yields soundness, that is, every proof admits a unique coalgebra-to-algebra morphism. We demonstrate our framework through a non-wellfounded proof system for the modal mu-calculus, one for higher-order fixed-point logics, and a non-wellfounded variant of Santocanale's circular proof system in mu-bicomplete categories.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper turns the global trace condition into recursiveness of a coalgebra image under an adjoint, giving soundness once an assumption on the algebra is granted.

read the letter

The main takeaway is that this work recasts the global trace condition for non-wellfounded proofs as the recursiveness of the coalgebra after a suitable adjoint is applied. That converts a global infinitary constraint on paths into a local recursive property, which is the central new move. They model derivation trees as coalgebras for generalized polynomial functors on presheaves, then use graphs of coalgebras to express the GTC as a condition on those graphs. The key equivalence states that a coalgebra satisfies the GTC if and only if its image under the adjoint is recursive. Under an assumption on the semantic algebra, this produces the unique coalgebra-to-algebra morphism that stands for soundness. The paper demonstrates the setup on a non-wellfounded system for the modal mu-calculus, a system for higher-order fixed-point logics, and a non-wellfounded variant of Santocanale's circular proofs in mu-bicomplete categories. These examples show the framework can be instantiated without collapsing into pure abstraction. The coalgebraic modeling and the reduction to recursive coalgebras look like genuine progress in organizing the infinitary condition. The constructions appear standard rather than circular, and the demonstrations give some concrete grounding. One soft spot is the dependence on that unspecified assumption on the semantic algebra to secure the unique morphism. The paper needs to state the assumption plainly and confirm it holds in the three examples without hidden extra conditions. If the assumption turns out mild and routinely satisfied, the result is fine; if it is strong, it narrows the scope. This is aimed at readers already working with coalgebras in proof theory or modal logics. Someone in that niche would find the reformulation useful for handling non-wellfounded systems. The work shows clear engagement with the literature and the math holds together on its own terms, so it deserves a serious referee rather than a desk reject.

Referee Report

1 major / 2 minor

Summary. The paper develops a coalgebraic framework for non-wellfounded proof systems in which derivation trees are modelled as coalgebras of generalised polynomial functors on presheaves. It reformulates the global trace condition (GTC) as a condition on graphs of coalgebras and proves that a coalgebra satisfies the GTC if and only if its image under a suitable adjoint is recursive. Under an appropriate assumption on the semantic algebra, this equivalence yields soundness in the form of a unique coalgebra-to-algebra morphism. The framework is illustrated on a non-wellfounded proof system for the modal mu-calculus, one for higher-order fixed-point logics, and a non-wellfounded variant of Santocanale's circular proof system in mu-bicomplete categories.

Significance. If the central equivalence holds, the work supplies a categorical characterisation that directly links the non-compositional GTC to the well-studied notion of recursive coalgebras, thereby offering a uniform method for establishing soundness across infinitary proof systems. The use of presheaf coalgebras and adjoints provides a technically coherent bridge between coalgebraic semantics and proof-theoretic soundness, and the three concrete demonstrations indicate that the framework can be instantiated for both modal and higher-order fixed-point logics. The absence of free parameters and the reduction to recursiveness constitute genuine strengths that could support future transfer of results between different non-wellfounded calculi.

major comments (1)

[paragraph following the main theorem on recursive coalgebras] The paragraph following the main theorem on recursive coalgebras states that soundness follows once an 'appropriate assumption' on the semantic algebra is granted. This assumption is load-bearing for the final step from recursiveness to the existence of a unique coalgebra-to-algebra morphism, yet its precise formulation is not given in the abstract and must be stated explicitly (with any necessary side conditions on the algebra) to allow verification that the implication holds in the demonstrated examples.

minor comments (2)

[Preliminaries] Notation for the generalised polynomial functors and the adjoint functor could be introduced with a short table or diagram in the preliminaries to improve readability when the same constructions are reused across the three case studies.
[Section on graphs of coalgebras] The description of the graph-of-coalgebras construction would benefit from an explicit commutative diagram showing how the GTC condition on infinite paths is expressed coalgebraically.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the positive assessment of our work and for the constructive comment regarding the formulation of the assumption on the semantic algebra. We address this point below.

read point-by-point responses

Referee: [paragraph following the main theorem on recursive coalgebras] The paragraph following the main theorem on recursive coalgebras states that soundness follows once an 'appropriate assumption' on the semantic algebra is granted. This assumption is load-bearing for the final step from recursiveness to the existence of a unique coalgebra-to-algebra morphism, yet its precise formulation is not given in the abstract and must be stated explicitly (with any necessary side conditions on the algebra) to allow verification that the implication holds in the demonstrated examples.

Authors: We agree that the assumption should be stated explicitly. While the assumption is formulated in the body of the paper, we acknowledge that its absence from the abstract hinders immediate verification. In the revised manuscript we will update the abstract to include a precise statement of the assumption together with any side conditions required for the unique coalgebra-to-algebra morphism to exist. This will make it straightforward to check that the condition applies to the three concrete examples (modal mu-calculus, higher-order fixed-point logics, and the non-wellfounded variant of Santocanale's system). revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained

full rationale

The paper constructs a coalgebraic model of derivation trees as coalgebras for generalised polynomial functors on presheaves, formulates the GTC on graphs of coalgebras, and proves the equivalence that a coalgebra satisfies the GTC precisely when its image under a suitable adjoint is recursive. Soundness (unique coalgebra-to-algebra morphism) then follows from a stated assumption on the semantic algebra. This chain relies on standard coalgebraic definitions and equivalences rather than any fitted parameter renamed as prediction, self-definitional loop, or load-bearing self-citation whose content reduces to the present result. The framework is therefore independent of its own outputs and self-contained against external coalgebraic theory.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The framework rests on standard category-theoretic background and the existence of suitable adjoints and recursive coalgebras; no free parameters or invented entities are introduced beyond the modelling choices themselves.

axioms (2)

domain assumption Generalised polynomial functors on presheaves admit the required coalgebraic structure for derivation trees.
Invoked when derivation trees are modelled as coalgebras.
ad hoc to paper The semantic algebra satisfies the 'appropriate assumption' that turns recursiveness into unique coalgebra-to-algebra morphisms.
Explicitly required for the soundness conclusion.

pith-pipeline@v0.9.0 · 5776 in / 1359 out tokens · 33181 ms · 2026-05-19T19:33:32.130039+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/ArithmeticFromLogic.lean LogicNat recovery / embed_injective / well-foundedLT unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

a coalgebra satisfies the GTC if and only if its image under a suitable adjoint is recursive... every proof admits a unique coalgebra-to-algebra morphism (Theorem 4.17, Proposition 4.14, Lemma 4.12)
IndisputableMonolith/Foundation/AbsoluteFloorClosure.lean absolute_floor_iff_bare_distinguishability unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

familial functors... graphs of coalgebras... well-foundedness of the graph of c is equivalent to recursiveness (Theorem 1.9)

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

38 extracted references · 38 canonical work pages

[1]

Free algebras and automata realizations in the language of categories

Jir \' Ad \' a mek. Free algebras and automata realizations in the language of categories. Commentationes Mathematicae Universitatis Carolinae , 015(4):589--602, 1974

work page 1974
[2]

Bahareh Afshari and Graham E. Leigh. Cut-free completeness for modal mu-calculus. In LICS , pages 1--12. IEEE Computer Society, 2017

work page 2017
[3]

Recursive coalgebras of finitary functors

Jir \' Ad \' a mek, Dominik L \" u cke, and Stefan Milius. Recursive coalgebras of finitary functors. RAIRO Theor. Informatics Appl. , 41(4):447--462, 2007

work page 2007
[4]

Jir \' Ad \' a mek, Stefan Milius, and Lawrence S. Moss. Fixed points of functors. J. Log. Algebraic Methods Program. , 95:41--81, 2018

work page 2018
[5]

Jir \' Ad \' a mek, Stefan Milius, and Lawrence S. Moss. On well-founded and recursive coalgebras. In Jean Goubault - Larrecq and Barbara K \" o nig, editors, Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 202...

work page 2020
[6]

Moss, and Lurdes Sousa

Jir \' Ad \' a mek, Stefan Milius, Lawrence S. Moss, and Lurdes Sousa. Well-pointed coalgebras. Log. Methods Comput. Sci. , 9(3), 2013

work page 2013
[7]

Abstract cyclic proofs

Bahareh Afshari and Dominik Wehr. Abstract cyclic proofs. In Logic, Language, Information, and Computation - 28th International Workshop, WoLLIC 2022, Ia s i, Romania, September 20-23, 2022, Proceedings , volume 13468 of Lecture Notes in Computer Science , pages 309--325. Springer, 2022

work page 2022
[8]

Bouncing threads for circular and non-wellfounded proofs: Towards compositionality with circular proofs

David Baelde, Amina Doumane, Denis Kuperberg, and Alexis Saurin. Bouncing threads for circular and non-wellfounded proofs: Towards compositionality with circular proofs. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science , LICS '22. Association for Computing Machinery, 2022

work page 2022
[9]

Alternating parity krivine automata

Florian Bruse. Alternating parity krivine automata. In MFCS (1) , volume 8634 of Lecture Notes in Computer Science , pages 111--122. Springer, 2014

work page 2014
[10]

Sequent calculi for induction and infinite descent

James Brotherston and Alex Simpson. Sequent calculi for induction and infinite descent. J. Log. Comput. , 21(6):1177--1216, 2011

work page 2011
[11]

An introduction to corecursive algebras, 2007

Venanzio Capretta. An introduction to corecursive algebras, 2007. Slide presentation. URL: https://people.cs.nott.ac.uk/pszvc/publications/brouwer_seminar_4_12_2007.pdf

work page 2007
[12]

Constructive versions of tarski’s fixed point theorems

Patrick Cousot and Radhia Cousot. Constructive versions of tarski’s fixed point theorems. Pacific journal of Mathematics , 82(1):43--57, 1979

work page 1979
[13]

Recursive coalgebras from comonads

Venanzio Capretta, Tarmo Uustalu, and Varmo Vene. Recursive coalgebras from comonads. Inf. Comput. , 204(4):437--468, 2006

work page 2006
[14]

Stream automata are coalgebras

Vincenzo Ciancia and Yde Venema. Stream automata are coalgebras. In CMCS , volume 7399 of Lecture Notes in Computer Science , pages 90--108. Springer, 2012

work page 2012
[15]

On the denotation of circular and non-wellfounded proofs in linear logic with fixed points

Thomas Ehrhard, Farzad Jafarrahmani, and Alexis Saurin. On the denotation of circular and non-wellfounded proofs in linear logic with fixed points. In 40th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2025, Singapore, June 23-26, 2025 , pages 84--97. IEEE , 2025

work page 2025
[16]

Marcelo P. Fiore. Discrete generalised polynomial functors - (extended abstract). In Artur Czumaj, Kurt Mehlhorn, Andrew M. Pitts, and Roger Wattenhofer, editors, Automata, Languages, and Programming - 39th International Colloquium, ICALP 2012, Warwick, UK, July 9-13, 2012, Proceedings, Part II , volume 7392 of Lecture Notes in Computer Science , pages 21...

work page 2012
[17]

Cuts for circular proofs: semantics and cut-elimination

J \' e r \^ o me Fortier and Luigi Santocanale. Cuts for circular proofs: semantics and cut-elimination. In Simona Ronchi Della Rocca, editor, Computer Science Logic 2013, CSL 2013, Torino, Italy, September 2-5, 2013 , volume 23 of LIPIcs , pages 248--262. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik, 2013

work page 2013
[18]

Polynomial functors and polynomial monads

Nicola Gambino and Joachim Kock. Polynomial functors and polynomial monads. In Mathematical proceedings of the cambridge philosophical society , volume 154, pages 153--192. Cambridge University Press, 2013

work page 2013
[19]

Peter Gumm

H. Peter Gumm. From T-coalgebras to filter structures and transition systems. In CALCO , volume 3629 of Lecture Notes in Computer Science , pages 194--212. Springer, 2005

work page 2005
[20]

Structural induction and coinduction in a fibrational setting

Claudio Hermida and Bart Jacobs. Structural induction and coinduction in a fibrational setting. Inf. Comput. , 145(2):107--152, 1998

work page 1998
[21]

Well-founded coalgebras, revisited

Jean - Baptiste Jeannin, Dexter Kozen, and Alexandra Silva. Well-founded coalgebras, revisited. Math. Struct. Comput. Sci. , 27(7):1111--1131, 2017

work page 2017
[22]

Realization of coinductive types

Dexter Kozen. Realization of coinductive types. In Michael W. Mislove and Jo \" e l Ouaknine, editors, Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics, MFPS 2011, Pittsburgh, PA, USA, May 25-28, 2011 , volume 276 of Electronic Notes in Theoretical Computer Science , pages 237--246. Elsevier, 2011

work page 2011
[23]

A cyclic proof system for hfl \_ \( n \)

Mayuko Kori, Takeshi Tsukada, and Naoki Kobayashi. A cyclic proof system for hfl \_ \( n \) . arXiv preprint arXiv:2010.14891 , 2020. URL: https://arxiv.org/abs/2010.14891

work page arXiv 2010
[24]

A cyclic proof system for hfl \_ \( n \)

Mayuko Kori, Takeshi Tsukada, and Naoki Kobayashi. A cyclic proof system for hfl \_ \( n \) . In CSL , volume 183 of LIPIcs , pages 29:1--29:22. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik, 2021

work page 2021
[25]

Categorical notions of fibration

Fosco Loregian and Emily Riehl. Categorical notions of fibration. Expositiones Mathematicae , 38(4):496--514, 2020

work page 2020
[26]

Leigh and Dominik Wehr

Graham E. Leigh and Dominik Wehr. From GTC to RESET : Generating reset proof systems from cyclic proof systems. Ann. Pure Appl. Log. , 175(10):103485, 2024

work page 2024
[27]

Games for the mu-calculus

Damian Niwinski and Igor Walukiewicz. Games for the mu-calculus. Theor. Comput. Sci. , 163(1 & 2):99--116, 1996

work page 1996
[28]

Categorical set theory: A characterization of the category of sets

Gerhard Osius. Categorical set theory: A characterization of the category of sets. Journal of Pure and Applied Algebra , 4(1):79--119, 1974

work page 1974
[29]

Andrew M. Pitts. Categorical logic , page 39–123. Oxford University Press, Inc., USA, 2001

work page 2001
[30]

Kan extensions are partial colimits

Paolo Perrone and Walter Tholen. Kan extensions are partial colimits. Applied Categorical Structures , 30(4):685--753, 2022

work page 2022
[31]

Steps and traces

Jurriaan Rot, Bart Jacobs, and Paul Blain Levy. Steps and traces. J. Log. Comput. , 31(6):1482--1525, 2021

work page 2021
[32]

Robert Rosebrugh and R.J. Wood. Proarrows and cofibrations. Journal of Pure and Applied Algebra , 53(3):271--296, 1988

work page 1988
[33]

\( \) -bicomplete categories and parity games

Luigi Santocanale. \( \) -bicomplete categories and parity games. RAIRO Theor. Informatics Appl. , 36(2):195--227, 2002

work page 2002
[34]

A calculus of circular proofs and its categorical semantics

Luigi Santocanale. A calculus of circular proofs and its categorical semantics. In FoSSaCS , Lecture Notes in Computer Science, pages 357--371. Springer, 2002

work page 2002
[35]

Practical Foundations of Mathematics , volume 59 of Cambridge studies in advanced mathematics

Paul Taylor. Practical Foundations of Mathematics , volume 59 of Cambridge studies in advanced mathematics . Cambridge University Press, 1999

work page 1999
[36]

Well founded coalgebras and recursion, 2021

Paul Taylor. Well founded coalgebras and recursion, 2021. preprint on webpage at https://www.paultaylor.eu/ordinals/welfcr.pdf. URL: https://www.paultaylor.eu/ordinals/welfcr.pdf

work page 2021
[37]

Categorical b \" u chi and parity conditions via alternating fixed points of functors

Natsuki Urabe and Ichiro Hasuo. Categorical b \" u chi and parity conditions via alternating fixed points of functors. In Corina C \^ rstea, editor, Coalgebraic Methods in Computer Science - 14th IFIP WG 1.3 International Workshop, CMCS 2018, Colocated with ETAPS 2018, Thessaloniki, Greece, April 14-15, 2018, Revised Selected Papers , volume 11202 of Lect...

work page 2018
[38]

Familial 2-functors and parametric right adjoints

Mark Weber. Familial 2-functors and parametric right adjoints. Theory and Applications of Categories [electronic only] , 18:665--732, 2007

work page 2007

[1] [1]

Free algebras and automata realizations in the language of categories

Jir \' Ad \' a mek. Free algebras and automata realizations in the language of categories. Commentationes Mathematicae Universitatis Carolinae , 015(4):589--602, 1974

work page 1974

[2] [2]

Bahareh Afshari and Graham E. Leigh. Cut-free completeness for modal mu-calculus. In LICS , pages 1--12. IEEE Computer Society, 2017

work page 2017

[3] [3]

Recursive coalgebras of finitary functors

Jir \' Ad \' a mek, Dominik L \" u cke, and Stefan Milius. Recursive coalgebras of finitary functors. RAIRO Theor. Informatics Appl. , 41(4):447--462, 2007

work page 2007

[4] [4]

Jir \' Ad \' a mek, Stefan Milius, and Lawrence S. Moss. Fixed points of functors. J. Log. Algebraic Methods Program. , 95:41--81, 2018

work page 2018

[5] [5]

Jir \' Ad \' a mek, Stefan Milius, and Lawrence S. Moss. On well-founded and recursive coalgebras. In Jean Goubault - Larrecq and Barbara K \" o nig, editors, Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 202...

work page 2020

[6] [6]

Moss, and Lurdes Sousa

Jir \' Ad \' a mek, Stefan Milius, Lawrence S. Moss, and Lurdes Sousa. Well-pointed coalgebras. Log. Methods Comput. Sci. , 9(3), 2013

work page 2013

[7] [7]

Abstract cyclic proofs

Bahareh Afshari and Dominik Wehr. Abstract cyclic proofs. In Logic, Language, Information, and Computation - 28th International Workshop, WoLLIC 2022, Ia s i, Romania, September 20-23, 2022, Proceedings , volume 13468 of Lecture Notes in Computer Science , pages 309--325. Springer, 2022

work page 2022

[8] [8]

Bouncing threads for circular and non-wellfounded proofs: Towards compositionality with circular proofs

David Baelde, Amina Doumane, Denis Kuperberg, and Alexis Saurin. Bouncing threads for circular and non-wellfounded proofs: Towards compositionality with circular proofs. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science , LICS '22. Association for Computing Machinery, 2022

work page 2022

[9] [9]

Alternating parity krivine automata

Florian Bruse. Alternating parity krivine automata. In MFCS (1) , volume 8634 of Lecture Notes in Computer Science , pages 111--122. Springer, 2014

work page 2014

[10] [10]

Sequent calculi for induction and infinite descent

James Brotherston and Alex Simpson. Sequent calculi for induction and infinite descent. J. Log. Comput. , 21(6):1177--1216, 2011

work page 2011

[11] [11]

An introduction to corecursive algebras, 2007

Venanzio Capretta. An introduction to corecursive algebras, 2007. Slide presentation. URL: https://people.cs.nott.ac.uk/pszvc/publications/brouwer_seminar_4_12_2007.pdf

work page 2007

[12] [12]

Constructive versions of tarski’s fixed point theorems

Patrick Cousot and Radhia Cousot. Constructive versions of tarski’s fixed point theorems. Pacific journal of Mathematics , 82(1):43--57, 1979

work page 1979

[13] [13]

Recursive coalgebras from comonads

Venanzio Capretta, Tarmo Uustalu, and Varmo Vene. Recursive coalgebras from comonads. Inf. Comput. , 204(4):437--468, 2006

work page 2006

[14] [14]

Stream automata are coalgebras

Vincenzo Ciancia and Yde Venema. Stream automata are coalgebras. In CMCS , volume 7399 of Lecture Notes in Computer Science , pages 90--108. Springer, 2012

work page 2012

[15] [15]

On the denotation of circular and non-wellfounded proofs in linear logic with fixed points

Thomas Ehrhard, Farzad Jafarrahmani, and Alexis Saurin. On the denotation of circular and non-wellfounded proofs in linear logic with fixed points. In 40th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2025, Singapore, June 23-26, 2025 , pages 84--97. IEEE , 2025

work page 2025

[16] [16]

Marcelo P. Fiore. Discrete generalised polynomial functors - (extended abstract). In Artur Czumaj, Kurt Mehlhorn, Andrew M. Pitts, and Roger Wattenhofer, editors, Automata, Languages, and Programming - 39th International Colloquium, ICALP 2012, Warwick, UK, July 9-13, 2012, Proceedings, Part II , volume 7392 of Lecture Notes in Computer Science , pages 21...

work page 2012

[17] [17]

Cuts for circular proofs: semantics and cut-elimination

J \' e r \^ o me Fortier and Luigi Santocanale. Cuts for circular proofs: semantics and cut-elimination. In Simona Ronchi Della Rocca, editor, Computer Science Logic 2013, CSL 2013, Torino, Italy, September 2-5, 2013 , volume 23 of LIPIcs , pages 248--262. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik, 2013

work page 2013

[18] [18]

Polynomial functors and polynomial monads

Nicola Gambino and Joachim Kock. Polynomial functors and polynomial monads. In Mathematical proceedings of the cambridge philosophical society , volume 154, pages 153--192. Cambridge University Press, 2013

work page 2013

[19] [19]

Peter Gumm

H. Peter Gumm. From T-coalgebras to filter structures and transition systems. In CALCO , volume 3629 of Lecture Notes in Computer Science , pages 194--212. Springer, 2005

work page 2005

[20] [20]

Structural induction and coinduction in a fibrational setting

Claudio Hermida and Bart Jacobs. Structural induction and coinduction in a fibrational setting. Inf. Comput. , 145(2):107--152, 1998

work page 1998

[21] [21]

Well-founded coalgebras, revisited

Jean - Baptiste Jeannin, Dexter Kozen, and Alexandra Silva. Well-founded coalgebras, revisited. Math. Struct. Comput. Sci. , 27(7):1111--1131, 2017

work page 2017

[22] [22]

Realization of coinductive types

Dexter Kozen. Realization of coinductive types. In Michael W. Mislove and Jo \" e l Ouaknine, editors, Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics, MFPS 2011, Pittsburgh, PA, USA, May 25-28, 2011 , volume 276 of Electronic Notes in Theoretical Computer Science , pages 237--246. Elsevier, 2011

work page 2011

[23] [23]

A cyclic proof system for hfl \_ \( n \)

Mayuko Kori, Takeshi Tsukada, and Naoki Kobayashi. A cyclic proof system for hfl \_ \( n \) . arXiv preprint arXiv:2010.14891 , 2020. URL: https://arxiv.org/abs/2010.14891

work page arXiv 2010

[24] [24]

A cyclic proof system for hfl \_ \( n \)

Mayuko Kori, Takeshi Tsukada, and Naoki Kobayashi. A cyclic proof system for hfl \_ \( n \) . In CSL , volume 183 of LIPIcs , pages 29:1--29:22. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik, 2021

work page 2021

[25] [25]

Categorical notions of fibration

Fosco Loregian and Emily Riehl. Categorical notions of fibration. Expositiones Mathematicae , 38(4):496--514, 2020

work page 2020

[26] [26]

Leigh and Dominik Wehr

Graham E. Leigh and Dominik Wehr. From GTC to RESET : Generating reset proof systems from cyclic proof systems. Ann. Pure Appl. Log. , 175(10):103485, 2024

work page 2024

[27] [27]

Games for the mu-calculus

Damian Niwinski and Igor Walukiewicz. Games for the mu-calculus. Theor. Comput. Sci. , 163(1 & 2):99--116, 1996

work page 1996

[28] [28]

Categorical set theory: A characterization of the category of sets

Gerhard Osius. Categorical set theory: A characterization of the category of sets. Journal of Pure and Applied Algebra , 4(1):79--119, 1974

work page 1974

[29] [29]

Andrew M. Pitts. Categorical logic , page 39–123. Oxford University Press, Inc., USA, 2001

work page 2001

[30] [30]

Kan extensions are partial colimits

Paolo Perrone and Walter Tholen. Kan extensions are partial colimits. Applied Categorical Structures , 30(4):685--753, 2022

work page 2022

[31] [31]

Steps and traces

Jurriaan Rot, Bart Jacobs, and Paul Blain Levy. Steps and traces. J. Log. Comput. , 31(6):1482--1525, 2021

work page 2021

[32] [32]

Robert Rosebrugh and R.J. Wood. Proarrows and cofibrations. Journal of Pure and Applied Algebra , 53(3):271--296, 1988

work page 1988

[33] [33]

\( \) -bicomplete categories and parity games

Luigi Santocanale. \( \) -bicomplete categories and parity games. RAIRO Theor. Informatics Appl. , 36(2):195--227, 2002

work page 2002

[34] [34]

A calculus of circular proofs and its categorical semantics

Luigi Santocanale. A calculus of circular proofs and its categorical semantics. In FoSSaCS , Lecture Notes in Computer Science, pages 357--371. Springer, 2002

work page 2002

[35] [35]

Practical Foundations of Mathematics , volume 59 of Cambridge studies in advanced mathematics

Paul Taylor. Practical Foundations of Mathematics , volume 59 of Cambridge studies in advanced mathematics . Cambridge University Press, 1999

work page 1999

[36] [36]

Well founded coalgebras and recursion, 2021

Paul Taylor. Well founded coalgebras and recursion, 2021. preprint on webpage at https://www.paultaylor.eu/ordinals/welfcr.pdf. URL: https://www.paultaylor.eu/ordinals/welfcr.pdf

work page 2021

[37] [37]

Categorical b \" u chi and parity conditions via alternating fixed points of functors

Natsuki Urabe and Ichiro Hasuo. Categorical b \" u chi and parity conditions via alternating fixed points of functors. In Corina C \^ rstea, editor, Coalgebraic Methods in Computer Science - 14th IFIP WG 1.3 International Workshop, CMCS 2018, Colocated with ETAPS 2018, Thessaloniki, Greece, April 14-15, 2018, Revised Selected Papers , volume 11202 of Lect...

work page 2018

[38] [38]

Familial 2-functors and parametric right adjoints

Mark Weber. Familial 2-functors and parametric right adjoints. Theory and Applications of Categories [electronic only] , 18:665--732, 2007

work page 2007