4 papers
Connectivity at the crossroad of intuitionistic and classical polarizations in linear logic
Raffaele Di Donna, Giulio Guerrieri, Lorenzo Tortora de Falco
We investigate a property that extends the Danos-Regnier correctness criterion for linear logic proof-structures. The property applies to the correctness graphs of a proof-structur…
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…
Closure Conversion, Flat Environments, and the Complexity of Abstract Machines
Beniamino Accattoli, Dan Ghica, Giulio Guerrieri +2
Closure conversion is a program transformation at work in compilers for functional languages to turn inner functions into global ones, by building closures pairing the transformed…