Bouncing threads for circular and non-wellfounded proofs. Towards compositionality with circular proofs
type: Item
instance of: scholarly article
title: Bouncing threads for circular and non-wellfounded proofs. Towards compositionality with circular proofs
DOI: 10.1145/3531130.3533375
author: David Baelde
author: Amina Doumane
author: Denis Kuperberg
author: Alexis Saurin
publication date: 2024-12-06T00:00:00Z
Mathematics Subject Classification ID: 03F07
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03F52
zbMATH DE Number: 7954878
zbMATH Keywords: circular proofs
zbMATH Keywords: coinduction
zbMATH Keywords: Curry-Howard correspondence
zbMATH Keywords: cut elimination
zbMATH Keywords: decidability
zbMATH Keywords: fixed points
zbMATH Keywords: linear logic
MaRDI profile type: MaRDI publication profile
cites work: Mixed Inductive/Coinductive Types and Strong Normalization
cites work: Well-founded recursion with copatterns and sized types
cites work: Copatterns
cites work: Least and Greatest Fixed Points in Linear Logic
cites work: Q5351980
cites work: Q5278431
cites work: Logical Reversibility of Computation
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: Sequent calculi for induction and infinite descent
cites work: Fair reactive programming
cites work: A Proof System for the Linear Time μ-Calculus
cites work: Infinets: the parallel syntax for non-wellfounded proof-theory
cites work: Q5144621
cites work: Towards Completeness via Proof Search in the Linear Time μ-calculus
cites work: Q2958526
cites work: Q4219036
cites work: Linear logic
cites work: Locus solum: From the rules of logic to the logic of rules.
cites work: Proof nets for unit-free multiplicative-additive linear logic
cites work: The Size-Change Termination Principle for Constructor Based Languages
cites work: Automata for the modal μ-calculus and related results
cites work: On modal mu-calculus and Büchi tree automata
cites work: Results on the propositional \(\mu\)-calculus
cites work: Q4263804
cites work: Inductive types and type constraints in the second-order lambda calculus
cites work: Recursive unsolvability of Post's problem of ''Tag'' und other topics in theory of Turing machines
cites work: Origins of bisimulation and coinduction
cites work: μ-Bicomplete Categories and Parity Games
cites work: Q4738237
cites work: Free \(\mu\)-lattices
cites work: An automata theoretic decision procedure for the propositional mu- calculus
cites work: Computational ludics
cites work: Completeness of Kozen's axiomatisation of the propositional \(\mu\)-calculus.
description: scientific article; zbMATH DE number 7954878