@inproceedings{114b3ccee3d2441eb34cd452fd04e69d,
title = "Infinitary Cut-Elimination via Finite Approximations",
abstract = "We investigate non-wellfounded proof systems based on parsimonious logic, a weaker variant of linear logic where the exponential modality ! is interpreted as a constructor for streams over finite data. Logical consistency is maintained at a global level by adapting a standard progressing criterion. We present an infinitary version of cut-elimination based on finite approximations, and we prove that, in presence of the progressing criterion, it returns well-defined non-wellfounded proofs at its limit. Furthermore, we show that cut-elimination preserves the progressing criterion and various regularity conditions internalizing degrees of proof-theoretical uniformity. Finally, we provide a denotational semantics for our systems based on the relational model.",
keywords = "approximation, cut-elimination, linear logic, non-uniform proofs, non-wellfounded proofs, parsimonious logic, proof theory, sequent calculus",
author = "Matteo Acclavio and Gianluca Curzi and Giulio Guerrieri",
year = "2024",
month = feb,
doi = "10.4230/LIPIcs.CSL.2024.8",
language = "English",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
editor = "Aniello Murano and Alexandra Silva",
booktitle = "32nd EACSL Annual Conference on Computer Science Logic, CSL 2024",
note = "32nd EACSL Annual Conference on Computer Science Logic, CSL 2024 ; Conference date: 19-02-2024 Through 23-02-2024",
}