6 papers
Making progress: Reducibility Candidates and Cut Elimination in the Ill-founded Realm
Gianluca Curzi, Graham E. Leigh
Ill-founded (or non-wellfounded) proof systems have emerged as a natural framework for inductive and coinductive reasoning. In such systems, soundness relies on global correctness…
Computational expressivity of (circular) proofs with fixed points
Gianluca Curzi, Anupam Das
We study the computational expressivity of proof systems with fixed point operators, within the 'proofs-as-programs' paradigm. We start with a calculus muLJ (due to Clairambault) t…
Non-wellfounded parsimonious proofs and non-uniform complexity
Matteo Acclavio, Gianluca Curzi, Giulio Guerrieri
In this paper we investigate the complexity-theoretical aspects of cyclic and non-wellfounded proofs in the context of parsimonious logic, a variant of linear logic where the expon…
Infinitary Cut-Elimination for Non-Wellfounded Parsimonious Linear Logic
Matteo Acclavio, Gianluca Curzi, Giulio Guerrieri
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 stre…
Cyclic Implicit Complexity
Gianluca Curzi, Anupam Das
Circular (or cyclic) proofs have received increasing attention in recent years, and have been proposed as an alternative setting for studying (co)inductive reasoning. In particular…
Cyclic proof theory of generalised inductive definitions
Gianluca Curzi, Lukas Melgaard
We study cyclic proof systems for , an extension of Peano arithmetic by positive inductive definitions that is arithmetically equivalent to the (impredicative) subsy…