Integrating induction and coinduction via closure operators and proof cycles
type: Item
instance of: scholarly article
title: Integrating induction and coinduction via closure operators and proof cycles
DOI: 10.1007/978-3-030-51074-9_21
author: Liron Cohen
author: Reuben N. S. Rowe
publication date: 2022-11-09T00:00:00Z
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7614523
describes a project that uses: Nuprl
describes a project that uses: CIRC
describes a project that uses: Irdis
describes a project that uses: CoCaml
describes a project that uses: CoALP
describes a project that uses: Agda
describes a project that uses: Idris
MaRDI profile type: Publication
full work available at URL: 978-3-030-51074-9 21
OpenAlex ID: W3039514567
cites work: Well-founded recursion with copatterns and sized types
cites work: Q5144634
cites work: Least and Greatest Fixed Points in Linear Logic
cites work: Q5278431
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: A Brief Overview of Agda – A Functional Language with Dependent Types
cites work: Idris, a general-purpose dependently typed programming language: Design and implementation
cites work: Formalised Inductive Reasoning in the Logic of Bunched Implications
cites work: Cyclic proofs of program termination in separation logic
cites work: Sequent calculi for induction and infinite descent
cites work: Handbook of proof theory
cites work: Completeness for ancestral logic via a computationally-meaningful semantics
cites work: Ancestral Logic: A Proof Theoretical Study
cites work: The middle ground-ancestral logic
cites work: Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent
cites work: Non-well-founded Proof Theory of Transitive Closure Logic
cites work: Towards automated reasoning in Herbrand structures
cites work: The relative efficiency of propositional proof systems
cites work: Fundamental properties of infinite trees
cites work: Q5079743
cites work: Q5144621
cites work: Q5277876
cites work: Q2958526
cites work: Recursive subtyping revealed
cites work: Untersuchungen über das logische Schliessen. I
cites work: Q2980965
cites work: A proof theory for model checking
cites work: Languages that Capture Complexity Classes
cites work: Q4355684
cites work: CoCaml: Functional Programming with Regular Coinductive Types
cites work: Coalgebraic Semantics for Derivations in Logic Programming
cites work: Practical coinduction
cites work: Coinductive big-step operational semantics
cites work: CIRC: A Circular Coinductive Prover
cites work: A homogeneous system for formal logic
cites work: Q5638283
cites work: Let’s See How Things Unfold: Reconciling the Infinite with the Intensional (Extended Abstract)
cites work: Cut-elimination for a logic with definitions and induction
cites work: Finiteness is mu-ineffable
cites work: Circular Coinduction: A Proof Theoretical Foundation
cites work: Universal coalgebra: A theory of systems
cites work: Q4738237
cites work: Q4001345
cites work: Co-Logic Programming: Extending Logic Programming with Coinduction
cites work: Coinductive Logic Programming
cites work: Cyclic Arithmetic Is Equivalent to Peano Arithmetic
cites work: Q4417874
cites work: Automatically verifying temporal properties of pointer programs with cyclic proof
cites work: Cut elimination for a logic with induction and co-induction
description: scientific article; zbMATH DE number 7614523