Coinduction in Flow: The Later Modality in Fibrations
From MaRDI portal
Publication:5875348
DOI10.4230/LIPICS.CALCO.2019.8OpenAlexW2991639264MaRDI QIDQ5875348FDOQ5875348
Authors: Henning Basold 
Publication date: 3 February 2023
Full work available at URL: http://doi.org/10.4230/LIPIcs.CALCO.2019.8
Recommendations
coinductionfibrationsprobabilistic programmingprobabilistic logicup-to techniquesrecursive proofslater modality
Cites Work
- The power of parameterization in coinductive proof
- Structural induction and coinduction in a fibrational setting
- Categorical logic and type theory
- Universal coalgebra: A theory of systems
- Coinductive predicates and final sequences in a fibration
- Title not available (Why is that?)
- Indexed induction and coinduction, fibrationally
- On traced monoidal closed categories
- Probabilistic systems coalgebraically: a survey
- Parametric corecursion
- Results on the propositional \(\mu\)-calculus
- Provability interpretations of modal logic
- Terminal coalgebras in well-founded set theory
- Strong functors and monoidal monads
- On the bisimulation proof method
- Coinduction up-to in a fibrational setting
- Circular coinduction: a proof theoretical foundation
- Behavioural differential equations: a coinductive calculus of streams, automata, and power series
- Parameter free induction and provably total computable functions
- Initial algebras and terminal coalgebras in many-sorted sets
- Title not available (Why is that?)
- Sequent calculi for induction and infinite descent
- Title not available (Why is that?)
- Title not available (Why is that?)
- Fibered categories and the foundations of naive category theory
- A very modal model of a modern, major, general type system
- Title not available (Why is that?)
- Co-Logic Programming: Extending Logic Programming with Coinduction
- Title not available (Why is that?)
- Complete Lattices and Up-To Techniques
- Enhanced coalgebraic bisimulation
- A Convenient Category for Higher-Order Probability Theory
- Inductive types and type constraints in the second-order lambda calculus
- μ-Bicomplete Categories and Parity Games
- Games for the \(\mu\)-calculus
- Truly modular (co)datatypes for Isabelle/HOL
- Title not available (Why is that?)
- Łukasiewicz \(\mu\)-calculus
- A Proof System for the Linear Time μ-Calculus
- Introduction to coalgebra. Towards mathematics of states and observation
- Deforestation, program transformation, and cut-elimination
- Guarded traced categories
- First steps in synthetic guarded domain theory: step-indexing in the topos of trees
- Guarded dependent type theory with coinductive types
- Sequent Calculus in the Topos of Trees
- A type theory for productive coprogramming via guarded recursion
- Productive coprogramming with guarded recursion
- Intensional type theory with guarded recursive types qua fixed points on universes
- Automated Reasoning with Analytic Tableaux and Related Methods
- Constructive completeness for the linear-time \(\mu \)-calculus
- Copatterns, programming infinite structures by observations
- Lifting adjunctions to coalgebras to (re)discover automata constructions
- Title not available (Why is that?)
- Cyclic arithmetic is equivalent to Peano arithmetic
- Coinduction All the Way Up
- Stream differential equations: specification formats and solution methods
- Companions, codensity and causality
- Monoidal company for accessible functors
- Guarded cubical type theory: path equality for guarded recursion
- Transfinite step-indexing: decoupling concrete and logical steps
- Dependent inductive and coinductive types are fibrational dialgebras
Uses Software
This page was built for publication: Coinduction in Flow: The Later Modality in Fibrations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5875348)
