19 citations · 55 across the 22 of their papers we have counts for
6 papers · 1 filter
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…