scientific article

DOI10.4230/LIPICS.CSL.2013.248zbMath1356.03098MaRDI QIDQ2958526

Jérôme Fortier, Luigi Santocanale

Publication date: 2 February 2017

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

fixpointsinductive and coinductive typescategorical proof-theoryinitial and final (co)algebras

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Proof theory in general (including proof-theoretic semantics) (03F03)

Related Items (19)

$\aleph_1$ and the modal $\mu$-calculus ⋮ Substructural Proofs as Automata ⋮ Unnamed Item ⋮ A logical framework with higher-order rational (circular) terms ⋮ Abstract cyclic proofs ⋮ Cyclic Arithmetic Is Equivalent to Peano Arithmetic ⋮ Unnamed Item ⋮ Abstract cyclic proofs ⋮ Coinduction in Flow: The Later Modality in Fibrations ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed-points ⋮ Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs ⋮ Cyclic implicit complexity ⋮ Bouncing threads for circular and non-wellfounded proofs. Towards compositionality with circular proofs ⋮ Non-well-founded deduction for induction and coinduction ⋮ NON-WELL-FOUNDED PROOFS FOR THE GRZEGORCZYK MODAL LOGIC ⋮ Integrating induction and coinduction via closure operators and proof cycles

This page was built for publication: