Buchumschlag

Compression for Coinductive Infinitary Rewriting: A Generic Approach, with Applications to Cut-Elimination for Non-Wellfounded Proofs

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Cerda, Rémy, Saurin, Alexis
Format:	Preprint
Veröffentlicht:	2025
Schlagworte:	Logic in Computer Science
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

Infinitary Cut-Elimination for Non-Wellfounded Parsimonious Linear Logic
von: Acclavio, Matteo, et al.
Veröffentlicht: (2023)

Coalgebraic Non-Wellfounded Proofs: Recursiveness and GTC
von: Kori, Mayuko
Veröffentlicht: (2026)

The Constructive $μ$-calculus: Game Semantics and Non-Wellfounded Proof Systems
von: Pacheco, Leonardo
Veröffentlicht: (2026)

Finitary Simulation of Infinitary $β$-Reduction via Taylor Expansion, and Applications
von: Cerda, Rémy, et al.
Veröffentlicht: (2022)

Nominal Algebraic-Coalgebraic Data Types, with Applications to Infinitary Lambda-Calculi
von: Cerda, Rémy
Veröffentlicht: (2025)

Ohana trees, linear approximation and multi-types for the $λ$I-calculus: No variable gets left behind or forgotten!
von: Cerda, Rémy, et al.
Veröffentlicht: (2025)

Coinductive Proofs for Temporal Hyperliveness
von: Correnson, Arthur, et al.
Veröffentlicht: (2025)

Formalising Inductive and Coinductive Containers
von: Damato, Stefania, et al.
Veröffentlicht: (2024)

A Semantic Proof of Generalised Cut Elimination for Deep Inference
von: Atkey, Robert, et al.
Veröffentlicht: (2024)

Proceedings Twelfth Workshop on Fixed Points in Computer Science
von: Saurin, Alexis
Veröffentlicht: (2025)

A Non-Wellfounded and Labelled Sequent Calculus for Bimodal Provability Logic
von: Becker, Justus
Veröffentlicht: (2025)

A Coinductive Reformulation of Milner's Proof System for Regular Expressions Modulo Bisimilarity
von: Grabmayer, Clemens
Veröffentlicht: (2022)

A uniform cut-elimination theorem for linear logics with fixed points and super exponentials
von: Bauer, Esaïe, et al.
Veröffentlicht: (2025)

Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
von: Kolesar, John, et al.
Veröffentlicht: (2025)

On the cut-elimination of the modal $μ$-calculus: Linear Logic to the rescue
von: Bauer, Esaïe, et al.
Veröffentlicht: (2025)

Hyperarithmetical Complexity of Infinitary Action Logic with Multiplexing
von: Pshenitsyn, Tikhon
Veröffentlicht: (2023)

CoLF Logic Programming as Infinitary Proof Exploration
von: Chen, Zhibo, et al.
Veröffentlicht: (2025)

Coinductive Techniques for Checking Satisfiability of Generalized Nested Conditions
von: Stoltenow, Lara, et al.
Veröffentlicht: (2024)

On the Cut Elimination of Weak Intuitionistic Tense Logic
von: Wang, Yiheng, et al.
Veröffentlicht: (2024)

A Curry-Howard Correspondence for Linear, Reversible Computation
von: Chardonnet, Kostia, et al.
Veröffentlicht: (2023)

The exponential logic of sequentialization
von: Alcolei, Aurore, et al.
Veröffentlicht: (2023)

Variable Elimination as Rewriting in a Linear Lambda Calculus
von: Ehrhard, Thomas, et al.
Veröffentlicht: (2025)

Coinductive Streams in Monoidal Categories
von: Di Lavore, Elena, et al.
Veröffentlicht: (2022)

Master Thesis Impredicative Encodings of Inductive and Coinductive Types
von: Bronsveld, Steven, et al.
Veröffentlicht: (2025)

The Size-Change Principle for Mixed Inductive and Coinductive types
von: Hyvernat, Pierre
Veröffentlicht: (2024)

Cut-Elimination for the Bimodal Logic GR
von: Kushida, Hirohiko
Veröffentlicht: (2026)

IMELL Cut Elimination with Linear Overhead
von: Accattoli, Beniamino, et al.
Veröffentlicht: (2024)

Algebraic Proof Theory for Infinitary Action Logic
von: Fussner, Wesley, et al.
Veröffentlicht: (2025)

Cut elimination for Cyclic Proofs: A Case Study in Temporal Logic
von: Afshari, Bahareh, et al.
Veröffentlicht: (2024)

Bidirectional Interpolation for the Lambda-Calculus -- Revisiting and Formalising Craig-Čubrić Interpolation
von: Bertrand, Meven Lennon, et al.
Veröffentlicht: (2026)

The Proof-Theoretic Origin of Double Negation Introduction & Elimination
von: Irani, Khashayar
Veröffentlicht: (2025)

Making progress: Reducibility Candidates and Cut Elimination in the Ill-founded Realm
von: Curzi, Gianluca, et al.
Veröffentlicht: (2026)

Syntactic Cut-Elimination for Provability Logic GL via Nested Sequents
von: Maniwa, Akinori, et al.
Veröffentlicht: (2024)

Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
von: Accattoli, Beniamino
Veröffentlicht: (2022)

Coinductive proof search for polarized logic with applications to full intuitionistic propositional logic
von: Santo, José Espírito, et al.
Veröffentlicht: (2020)

Tree Rewriting Calculi for Strictly Positive Logics
von: Santiago-Fernández, Sofía, et al.
Veröffentlicht: (2025)

Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures
von: Wernhard, Christoph, et al.
Veröffentlicht: (2025)

Proofs that Modify Proofs, 1/2
von: Towsner, Henry
Veröffentlicht: (2025)

Drag Rewriting
von: Dershowitz, Nachum, et al.
Veröffentlicht: (2024)

A Topological Rewriting of Tarski's Mereogeometry
von: Barlatier, Patrick, et al.
Veröffentlicht: (2025)