Coinduction in Flow: The Later Modality in Fibrations
From MaRDI portal
Publication:5875348
DOI10.4230/LIPIcs.CALCO.2019.8OpenAlexW2991639264MaRDI QIDQ5875348
Publication date: 3 February 2023
Full work available at URL: http://doi.org/10.4230/LIPIcs.CALCO.2019.8
fibrationsprobabilistic programmingcoinductionprobabilistic logicup-to techniquesrecursive proofslater modality
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Coinductive predicates and final sequences in a fibration
- Probabilistic systems coalgebraically: a survey
- Games for the \(\mu\)-calculus
- Results on the propositional \(\mu\)-calculus
- Provability interpretations of modal logic
- Structural induction and coinduction in a fibrational setting
- Categorical logic and type theory
- Universal coalgebra: A theory of systems
- Guarded traced categories
- Behavioural differential equations: a coinductive calculus of streams, automata, and power series
- Parameter free induction and provably total computable functions
- Terminal coalgebras in well-founded set theory
- Strong functors and monoidal monads
- Inductive types and type constraints in the second-order lambda calculus
- Transfinite Step-Indexing: Decoupling Concrete and Logical Steps
- Guarded Dependent Type Theory with Coinductive Types
- Introduction to Coalgebra
- Truly Modular (Co)datatypes for Isabelle/HOL
- Circular Coinduction: A Proof Theoretical Foundation
- Copatterns
- The power of parameterization in coinductive proof
- Lifting Adjunctions to Coalgebras to (Re)Discover Automata Constructions
- Sequent Calculus in the Topos of Trees
- Companions, Codensity and Causality
- Cyclic Arithmetic Is Equivalent to Peano Arithmetic
- Initial algebras and terminal coalgebras in many-sorted sets
- Sequent calculi for induction and infinite descent
- First steps in synthetic guarded domain theory: step-indexing in the topos of trees
- A very modal model of a modern, major, general type system
- Complete Lattices and Up-To Techniques
- On traced monoidal closed categories
- Fibered categories and the foundations of naive category theory
- On the bisimulation proof method
- Łukasiewicz μ-calculus
- Coinduction up-to in a fibrational setting
- A type theory for productive coprogramming via guarded recursion
- Coinduction All the Way Up
- μ-Bicomplete Categories and Parity Games
- Deforestation, program transformation, and cut-elimination
- A Convenient Category for Higher-Order Probability Theory
- Productive coprogramming with guarded recursion
- Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes
- Guarded Cubical Type Theory: Path Equality for Guarded Recursion
- Enhanced coalgebraic bisimulation
- A Proof System for the Linear Time μ-Calculus
- Co-Logic Programming: Extending Logic Programming with Coinduction
- Automated Reasoning with Analytic Tableaux and Related Methods
- Indexed Induction and Coinduction, Fibrationally
- Parametric corecursion
This page was built for publication: Coinduction in Flow: The Later Modality in Fibrations
