Jumping Boxes. - Beniamino Accattoli; Stefano Guerrini (CSL, 2009)

The Structural lambda-Calculus. - Beniamino Accattoli; Delia Kesner (CSL, 2010)

Proof Pearl: Abella Formalization of λ-Calculus Cube Property. - Beniamino Accattoli (CPP, 2012)

Call-by-Value Solvability, Revisited. - Beniamino Accattoli; Luca Paolini (FLOPS, 2012)

The Permutative λ-Calculus. - Beniamino Accattoli; Delia Kesner (LPAR, 2012)

An Abstract Factorization Theorem for Explicit Substitutions. - Beniamino Accattoli (RTA, 2012)

On the Invariance of the Unitary Cost Model for Head Reduction. - Beniamino Accattoli; Ugo Dal Lago (RTA, 2012)

On the Invariance of the Unitary Cost Model for Head Reduction (Long Version) - Beniamino Accattoli; Ugo Dal Lago (CoRR, 2012)

Preservation of Strong Normalisation modulo permutations for the structural lambda-calculus - Beniamino Accattoli; Delia Kesner (Log. Methods Comput. Sci., 2012)

Proof nets and the call-by-value lambda-calculus - Beniamino Accattoli (LSFA, 2012)

Compressing Polarized Boxes. - Beniamino Accattoli (LICS, 2013)

Linear Logic and Strong Normalization. - Beniamino Accattoli (RTA, 2013)

Evaluating functions as processes - Beniamino Accattoli (TERMGRAPH, 2013)

Beta reduction is invariant, indeed. - Beniamino Accattoli; Ugo Dal Lago (CSL-LICS, 2014)

Distilling abstract machines. - Beniamino Accattoli; Pablo Barenbaum; Damiano Mazza (ICFP, 2014)

A nonstandard standardization theorem. - Beniamino Accattoli; Eduardo Bonelli; Delia Kesner; Carlos Lombardi (POPL, 2014)

On the Value of Variables. - Beniamino Accattoli; Claudio Sacerdoti Coen (WoLLIC, 2014)

Distilling Abstract Machines (Long Version). - Beniamino Accattoli; Pablo Barenbaum; Damiano Mazza (CoRR, 2014)

Beta Reduction is Invariant, Indeed (Long Version). - Beniamino Accattoli; Ugo Dal Lago (CoRR, 2014)

A Strong Distillery. - Beniamino Accattoli; Pablo Barenbaum; Damiano Mazza (APLAS, 2015)

On the Relative Usefulness of Fireballs. - Beniamino Accattoli; Claudio Sacerdoti Coen (LICS, 2015)

Proof nets and the call-by-value λ-calculus. - Beniamino Accattoli (Theor. Comput. Sci., 2015)

Open Call-by-Value. - Beniamino Accattoli; Giulio Guerrieri (APLAS, 2016)

The Useful MAM, a Reasonable Implementation of the Strong λ-Calculus. - Beniamino Accattoli (WoLLIC, 2016)

The Complexity of Abstract Machines. - Beniamino Accattoli (WPTE@FSCD, 2016)

Open Call-by-Value (Extended Version). - Beniamino Accattoli; Giulio Guerrieri (CoRR, 2016)

(Leftmost-Outermost) Beta Reduction is Invariant, Indeed. - Beniamino Accattoli; Ugo Dal Lago (Log. Methods Comput. Sci., 2016)

The Negligible and Yet Subtle Cost of Pattern Matching. - Beniamino Accattoli; Bruno Barras (APLAS, 2017)

Implementing Open Call-by-Value. - Beniamino Accattoli; Giulio Guerrieri (FSEN, 2017)

Environments and the complexity of abstract machines. - Beniamino Accattoli; Bruno Barras (PPDP, 2017)

Implementing Open Call-by-Value (Extended Version). - Beniamino Accattoli; Giulio Guerrieri (CoRR, 2017)

Encoding Turing Machines into the Deterministic Lambda-Calculus. - Ugo Dal Lago; Beniamino Accattoli (CoRR, 2017)

The Maximal MAM, a Reasonable Implementation of the Maximal Strategy. - Beniamino Accattoli (CoRR, 2017)

(In)Efficiency and Reasonable Cost Models. - Beniamino Accattoli (LSFA, 2017)

Types of Fireballs. - Beniamino Accattoli; Giulio Guerrieri (APLAS, 2018)

Proof Nets and the Linear Substitution Calculus. - Beniamino Accattoli (ICTAC, 2018)

Types of Fireballs (Extended Version). - Beniamino Accattoli; Giulio Guerrieri (CoRR, 2018)

Preface. - Beniamino Accattoli; Carlos Olarte (LSFA, 2018)

Tight typings and split bounds. - Beniamino Accattoli; Stéphane Graham-Lengrand; Delia Kesner (Proc. ACM Program. Lang., 2018)

Factorization and Normalization, Essentially. - Beniamino Accattoli; Claudia Faggian; Giulio Guerrieri (APLAS, 2019)

Types by Need. - Beniamino Accattoli; Giulio Guerrieri; Maico Leberle (ESOP, 2019)

Crumbling Abstract Machines. - Beniamino Accattoli; Andrea Condoluci; Giulio Guerrieri; Claudio Sacerdoti Coen (PPDP, 2019)

Sharing Equality is Linear. - Andrea Condoluci; Beniamino Accattoli; Claudio Sacerdoti Coen (PPDP, 2019)

A Fresh Look at the lambda-Calculus (Invited Talk). - Beniamino Accattoli (FSCD, 2019)

Types by Need (Extended Version). - Beniamino Accattoli; Giulio Guerrieri; Maico Leberle (CoRR, 2019)

Abstract machines for Open Call-by-Value. - Beniamino Accattoli; Giulio Guerrieri (Sci. Comput. Program., 2019)

Functional Pearl: The Distributive λ-Calculus. - Beniamino Accattoli; Alejandro Díaz-Caro (FLOPS, 2020)

The Machinery of Interaction. - Beniamino Accattoli; Ugo Dal Lago; Gabriele Vanoni (PPDP, 2020)

The Abstract Machinery of Interaction (Long Version). - Ugo Dal Lago; Beniamino Accattoli; Gabriele Vanoni (CoRR, 2020)

Tight typings and split bounds, fully developed. - Beniamino Accattoli; Stéphane Graham-Lengrand; Delia Kesner (J. Funct. Program., 2020)

Factorize Factorization. - Beniamino Accattoli; Claudia Faggian; Giulio Guerrieri (CSL, 2021)

Strong Call-by-Value is Reasonable, Implosively. - Beniamino Accattoli; Andrea Condoluci; Claudio Sacerdoti Coen (LICS, 2021)

The Space of Interaction. - Beniamino Accattoli; Ugo Dal Lago; Gabriele Vanoni (LICS, 2021)

The Space of Interaction (long version). - Beniamino Accattoli; Ugo Dal Lago; Gabriele Vanoni (CoRR, 2021)

Semantic Bounds and Strong Call-by-Value Normalization. - Beniamino Accattoli; Giulio Guerrieri; Maico Leberle (CoRR, 2021)

The (In)Efficiency of interaction. - Beniamino Accattoli; Ugo Dal Lago; Gabriele Vanoni (Proc. ACM Program. Lang., 2021)

Useful Open Call-By-Need. - Beniamino Accattoli; Maico Leberle (CSL, 2022)

Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic. - Beniamino Accattoli (LICS, 2022)

Reasonable Space for the λ-Calculus, Logarithmically. - Beniamino Accattoli; Ugo Dal Lago; Gabriele Vanoni (LICS, 2022)

Call-by-Value Solvability and Multi Types. - Beniamino Accattoli; Giulio Guerrieri (CoRR, 2022)

The Theory of Call-by-Value Solvability (long version). - Beniamino Accattoli; Giulio Guerrieri (CoRR, 2022)

Multi Types and Reasonable Space (Long Version). - Beniamino Accattoli; Ugo Dal Lago; Gabriele Vanoni (CoRR, 2022)

The theory of call-by-value solvability. - Beniamino Accattoli; Giulio Guerrieri (Proc. ACM Program. Lang., 2022)

Multi types and reasonable space. - Beniamino Accattoli; Ugo Dal Lago; Gabriele Vanoni (Proc. ACM Program. Lang., 2022)

A Diamond Machine for Strong Evaluation. - Beniamino Accattoli; Pablo Barenbaum (APLAS, 2023)

Strong Call-by-Value and Multi Types. - Beniamino Accattoli; Giulio Guerrieri; Maico Leberle (ICTAC, 2023)

Formalizing Functions as Processes. - Beniamino Accattoli; Horace Blanc; Claudio Sacerdoti Coen (ITP, 2023)

Sharing a Perspective on the λ-Calculus. - Beniamino Accattoli (Onward!, 2023)

A Log-Sensitive Encoding of Turing Machines in the λ-Calculus. - Beniamino Accattoli; Ugo Dal Lago; Gabriele Vanoni (CoRR, 2023)

Normal Form Bisimulations By Value. - Beniamino Accattoli; Claudia Faggian; Adrienne Lancelot (CoRR, 2023)

Semantic Bound and Multi Types, Revisited. - Beniamino Accattoli (CoRR, 2023)

Semantic Bounds and Multi Types, Revisited. - Beniamino Accattoli (CSL, 2024)

Light Genericity. - Beniamino Accattoli; Adrienne Lancelot (FoSSaCS (2), 2024)

IMELL Cut Elimination with Linear Overhead. - Beniamino Accattoli; Claudio Sacerdoti Coen (FSCD, 2024)

Mirroring Call-By-Need, or Values Acting Silly. - Beniamino Accattoli; Adrienne Lancelot (FSCD, 2024)

Positive Focusing is Directly Useful. - Beniamino Accattoli; Jui-Hsuan Wu (CoRR, 2024)

Positive Sharing and Abstract Machines. - Beniamino Accattoli; Claudio Sacerdoti Coen; Jui-Hsuan Wu (APLAS, 2025)

The Vanilla Sequent Calculus is Call-by-Value. - Beniamino Accattoli (ESOP (1), 2025)

The Cost of Skeletal Call-By-Need, Smoothly. - Beniamino Accattoli; Francesco Magliocca; Loïc Peyrot; Claudio Sacerdoti Coen (FSCD, 2025)

Barendregt's Theory of the λ-Calculus, Refreshed and Formalized. - Adrienne Lancelot; Beniamino Accattoli; Maxime Vemclefs (ITP, 2025)

Interaction Equivalence. - Beniamino Accattoli; Adrienne Lancelot; Giulio Manzonetto; Gabriele Vanoni (Proc. ACM Program. Lang., 2025)

Closure Conversion, Flat Environments, and the Complexity of Abstract Machines. - Beniamino Accattoli; Dan Ghica; Giulio Guerrieri; Cláudio Belo Lourenço; Claudio Sacerdoti Coen (CoRR, 2025)