2 citations · 2 across the 6 of their papers we have counts for
11 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…
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) subsys…
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…
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-uniform complexity via non-wellfounded proofs
Gianluca Curzi, Anupam Das
Cyclic and non-wellfounded proofs are now increasingly employed to establish metalogical results in a variety of settings, in particular for type systems with forms of (co)inductio…
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…
Linear Additives
Gianluca Curzi
We introduce LAM, a subsystem of IMALL2 with restricted additive rules able to manage duplication linearly, called linear additive rules. LAM is presented as the type assignment sy…
Probabilistic Soft Type Assignment
Gianluca Curzi, Luca Roversi
We model randomized complexity classes in the style of Implicit Computational Complexity. We introduce PSTA, a probabilistic version of STA, the type-theoretical counterpart of Sof…
The Benefit of Being Non-Lazy in Probabilistic λ-calculus
Gianluca Curzi, Michele Pagani
We consider the probabilistic applicative bisimilarity (PAB), a coinductive relation comparing the applicative behaviour of probabilistic untyped lambda terms according to a specif…
A type-assignment of linear erasure and duplication
Gianluca Curzi, Luca Roversi
We introduce , a type-assignment system for the linear -calculus that extends second-order , i.e., intuitionistic multiplicative Linear Logic, by…