Bouncing threads for circular and non-wellfounded proofs. Towards compositionality with circular proofs

DOI10.1145/3531130.3533375MaRDI QIDQ6649500

Amina Doumane, Denis Kuperberg, David Baelde, Alexis Saurin

Publication date: 6 December 2024

fixed points cut elimination decidability linear logic Curry-Howard correspondence coinduction circular proofs

Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Cites Work

Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
Computational ludics
Linear logic
Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
Recursive unsolvability of Post's problem of Tag und other topics in theory of Turing machines
Results on the propositional \(\mu\)-calculus
An automata theoretic decision procedure for the propositional mu- calculus
On modal mu-calculus and Büchi tree automata
Completeness of Kozen's axiomatisation of the propositional \(\mu\)-calculus.
Infinets: the parallel syntax for non-wellfounded proof-theory
Inductive types and type constraints in the second-order lambda calculus
Locus solum: From the rules of logic to the logic of rules.
Copatterns
Sequent calculi for induction and infinite descent
Mixed Inductive/Coinductive Types and Strong Normalization
Automata for the modal μ-calculus and related results
Towards Completeness via Proof Search in the Linear Time μ-calculus
μ-Bicomplete Categories and Parity Games
Proof nets for unit-free multiplicative-additive linear logic
Well-founded recursion with copatterns and sized types
A Proof System for the Linear Time μ-Calculus
The Size-Change Termination Principle for Constructor Based Languages
Fair reactive programming
Origins of bisimulation and coinduction
Logical Reversibility of Computation
Least and Greatest Fixed Points in Linear Logic
Free \(\mu\)-lattices

This page was built for publication: Bouncing threads for circular and non-wellfounded proofs. Towards compositionality with circular proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6649500)