Structural induction and coinduction in a fibrational setting

DOI10.1006/inco.1998.2725zbMath0941.18006OpenAlexW2086788473MaRDI QIDQ1275820

Claudio Hermida, Bart Jacobs

Publication date: 31 July 2000

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/0e1b0f6284a7b6d286dea2363285667f85cda81b

zbMATH Keywords

recursive data typesinductionfibrationcategorical logiccoinduction

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Algebraic logic (03G99) Categories of machines, automata (18B20) Higher-type and set recursion theory (03D65)

Related Items (66)

Coinductive predicates and final sequences in a fibration ⋮ A Note on Hyperspaces and Terminal Coalgebras ⋮ Relating Coalgebraic Notions of Bisimulation ⋮ Logical relations and parametricity -- a Reynolds programme for category theory and programming languages ⋮ Coalgebraic modal logic: soundness, completeness and decidability of local consequence ⋮ The construction of set-truncated higher inductive types ⋮ De Bakker-Zucker processes revisited ⋮ Relation lifting, a survey ⋮ Recursively defined metric spaces without contraction ⋮ A Categorical Setting for Lower Complexity ⋮ Bisimulation as a logical relation ⋮ Structural Operational Semantics and Modal Logic, Revisited ⋮ Structural congruence for bialgebraic semantics ⋮ A coalgebraic perspective on logical interpretations ⋮ Safe recursion revisited. I: Categorical semantics for lower complexity ⋮ A Formalized Hierarchy of Probabilistic System Types ⋮ Unnamed Item ⋮ Generic weakest precondition semantics from monads enriched with order ⋮ Preservation and reflection of bisimilarity via invertible steps ⋮ Polarized subtyping ⋮ Unnamed Item ⋮ Enhanced coalgebraic bisimulation ⋮ Practical coinduction ⋮ Observational ultraproducts of polynomial coalgebras. ⋮ Coalgebras in functional programming and type theory ⋮ Bialgebras for structural operational semantics: an introduction ⋮ Unnamed Item ⋮ Coalgebraic trace semantics via forgetful logics ⋮ Generalized Eilenberg Theorem ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Coinduction in Flow: The Later Modality in Fibrations ⋮ Up-To Techniques for Behavioural Metrics via Fibrations ⋮ An Isbell duality theorem for type refinement systems ⋮ Coalgebraic minimization of automata by initiality and finality ⋮ Codensity Lifting of Monads and its Dual ⋮ Extensional quotient coalgebras ⋮ Generalised powerlocales via relation lifting ⋮ Many-Sorted Coalgebraic Modal Logic: a Model-theoretic Study ⋮ Coalgebras for Binary Methods: Properties of Bisimulations and Invariants ⋮ A general account of coinduction up-to ⋮ Process Calculi à la Bird-Meertens ⋮ A Calculus of Terms for Coalgebras of Polynomial Functors ⋮ Modal Languages for Coalgebras in a Topological Setting ⋮ Bialgebraic Semantics and Recursion ⋮ Transitivity and Difunctionality of Bisimulations ⋮ Duality of Equations and Coequations via Contravariant Adjunctions ⋮ Simulations in coalgebra ⋮ Expressive logics for coalgebras via terminal sequence induction ⋮ A modular approach to defining and characterising notions of simulation ⋮ Coalgebraic description of generalised binary methods ⋮ Bisimulation and coinduction enhancements: a historical perspective ⋮ Fibrational bisimulations and quantitative reasoning ⋮ Initial Algebra Semantics for Cyclic Sharing Structures ⋮ Extending set functors to generalised metric spaces ⋮ A categorical outlook on relational modalities and simulations ⋮ Coinductive predicates and final sequences in a fibration ⋮ Comprehension for Coalgebras ⋮ Greatest Bisimulations for Binary Methods ⋮ Induction, Coinduction, and Adjoints ⋮ Some properties of Fib as a fibred \(2\)-category ⋮ Universal coalgebra: A theory of systems ⋮ Unnamed Item ⋮ Predicate and relation liftings for coalgebras with side effects: an application in coalgebraic modal logic ⋮ Coalgebraic semantics for nominal automata ⋮ Corecursion up-to via causal transformations

Cites Work

• Strong categorical datatypes II: A term logic for categorical programming
• List-arithmetic distributive categories: Locoi
• Solving reflexive domain equations in a category of complete metric spaces
• New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic
• Algebraically compact functors
• Comprehension categories and the semantics of type dependency
• Categories of chain-complete posets
• Yoneda structures on 2-categories
• Some properties of Fib as a fibred \(2\)-category
• The fibrational formulation of intuitionistic predicate logic. I: Completeness according to Gödel, Kripke, and Läuchli. Part 2
• The fibrational formulation of intuitionistic predicate logic. I: Completeness according to Gödel, Kripke, and Läuchli. Part 1
• A co-induction principle for recursively defined domains
• Semantics of weakening and contraction
• Relational properties of domains
• A coinduction principle for recursive data types based on bisimulation
• The formal theory of monads
• Elementary observations on 2-categorical limits
• Algebraic specification of data types: A synthetic approach
• The Category-Theoretic Solution of Recursive Domain Equations
• Categories for Types
• Axiomatic Domain Theory in Categories of Partial Maps
• Parametrized data types do not need highly constrained parameters
• An approach to object semantics based on terminal co-algebras
• Fibrations with indeterminates: contextual and functional completeness for polymorphic lambda calculi
• A final coalgebra theorem
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Structural induction and coinduction in a fibrational setting