19 citations · 55 across the 22 of their papers we have counts for
31 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…
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…
The Benefits of Diligence
Victor Arrial, Giulio Guerrieri, Delia Kesner
This paper studies the strength of embedding Call-by-Name ({\tt dCBN}) and Call-by-Value ({\tt dCBV}) into a unifying framework called the Bang Calculus ({\tt dBANG}). These embedd…
Meaningfulness and Genericity in a Subsuming Framework
Delia Kesner, Victor Arrial, Giulio Guerrieri
This paper studies the notion of meaningfulness for a unifying framework called dBang-calculus, which subsumes both call-by-name (dCbN) and call-by-value (dCbV). We first character…
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…
Genericity Through Stratification
Victor Arrial, Giulio Guerrieri, Delia Kesner
A fundamental issue in the -calculus is to find appropriate notions for meaningfulness. It is well-known that in the call-by-name -calculus (CbN) the meaningful terms can be…
Strong Call-by-Value and Multi Types
Beniamino Accattoli, Giulio Guerrieri, Maico Leberle
This paper provides foundations for strong (that is, possibly under abstraction) call-by-value evaluation for the lambda-calculus. Recently, Accattoli et al. proposed a form of cal…
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…
The Theory of Call-by-Value Solvability (long version)
Beniamino Accattoli, Giulio Guerrieri
The denotational semantics of the untyped lambda-calculus is a well developed field built around the concept of solvable terms, which are elegantly characterized in many different…
Strategies for Asymptotic Normalization
Claudia Faggian, Giulio Guerrieri
We present a technique to study normalizing strategies when termination is asymptotic, that is, it appears as a limit, as opposite to reaching a normal form in a finite number of s…
Call-by-Value Solvability and Multi Types
Beniamino Accattoli, Giulio Guerrieri
This paper provides a characterization of call-by-value solvability using call-by-value multi types. Our work is based on Accattoli and Paolini's characterization of call-by-value…
A Deep Inference System for Differential Linear Logic
Matteo Acclavio, Giulio Guerrieri
Differential linear logic (DiLL) provides a fine analysis of resource consumption in cut-elimination. We investigate the subsystem of DiLL without promotion in a deep inference for…
Semantic Bounds and Strong Call-by-Value Normalization
Beniamino Accattoli, Giulio Guerrieri, Maico Leberle
This paper explores two topics at once: the use of denotational semantics to bound the evaluation length of functional programs, and the semantics of strong (that is, possibly unde…
On reduction and normalization in the computational core
Claudia Faggian, Giulio Guerrieri, Ugo de'Liguoro +1
We study the reduction in a lambda-calculus derived from Moggi's computational one, that we call the computational core. The reduction relation consists of rules obtained by orient…
Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic (long version)
Claudia Faggian, Giulio Guerrieri
In each variant of the lambda-calculus, factorization and normalization are two key-properties that show how results are computed. Instead of proving factorization/normalization fo…
Gluing resource proof-structures: inhabitation and inverting the Taylor expansion
Giulio Guerrieri, Luc Pellissier, Lorenzo Tortora de Falco
A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be expanded into a set of resource proof-structures: its Taylor expansion. We introduce a new criterion charact…
Factorize Factorization
Beniamino Accattoli, Claudia Faggian, Giulio Guerrieri
Factorization -- a simple form of standardization -- is concerned with reduction strategies, i.e. how a result is computed. We present a new technique for proving factorization the…
Decomposing Probabilistic Lambda-calculi
Ugo Dal Lago, Giulio Guerrieri, Willem Heijltjes
A notion of probabilistic lambda-calculus usually comes with a prescribed reduction strategy, typically call-by-name or call-by-value, as the calculus is non-confluent and these st…
Glueability of resource proof-structures: inverting the Taylor expansion (long version)
Giulio Guerrieri, Luc Pellissier, Lorenzo Tortora de Falco
A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be expanded into a set of resource proof-structures: its Taylor expansion. We introduce a new criterion charact…
Factorization and Normalization, Essentially
Beniamino Accattoli, Claudia Faggian, Giulio Guerrieri
Lambda-calculi come with no fixed evaluation strategy. Different strategies may then be considered, and it is important that they satisfy some abstract rewriting property, such as…
Crumbling Abstract Machines
Beniamino Accattoli, Andrea Condoluci, Giulio Guerrieri +1
Extending the lambda-calculus with a construct for sharing, such as let expressions, enables a special representation of terms: iterated applications are decomposed by introducing…
Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus
Giulio Guerrieri
We investigate the possibility of a semantic account of the execution time (i.e. the number of beta-steps leading to the normal form, if any) for the shuffling calculus, an extensi…
The Bang Calculus and the Two Girard's Translations
Giulio Guerrieri, Giulio Manzonetto
We study the two Girard's translations of intuitionistic implication into linear logic by exploiting the bang calculus, a paradigmatic functional language with an explicit box-oper…
Types by Need (Extended Version)
Beniamino Accattoli, Giulio Guerrieri, Maico Leberle
A cornerstone of the theory of lambda-calculus is that intersection types characterise termination properties. They are a flexible tool that can be adapted to various notions of te…