Beniamino Accattoli

109 papers A* 7A 2B 21C 9Misc 2Journal 54Unranked 13

Year	Rank	Type	Title / Venue / Authors
2025	B	`conf`	Barendregt's Theory of the λ-Calculus, Refreshed and Formalized. ITP Adrienne Lancelot, Beniamino Accattoli, Maxime Vemclefs
2025	C	`conf`	Closure Conversion, Flat Environments, and the Complexity of Abstract Machines. PPDP Beniamino Accattoli, Cláudio Belo Lourenço, Dan R. Ghica, Giulio Guerrieri, Claudio Sacerdoti Coen
2025	J	`jnl`	Closure Conversion, Flat Environments, and the Complexity of Abstract Machines. CoRR Beniamino Accattoli, Dan R. Ghica, Giulio Guerrieri, Cláudio Belo Lourenço, Claudio Sacerdoti Coen
2025	J	`jnl`	Interaction Equivalence. Proc. ACM Program. Lang. Beniamino Accattoli, Adrienne Lancelot, Giulio Manzonetto, Gabriele Vanoni
2025	B	`conf`	Positive Sharing and Abstract Machines. APLAS Beniamino Accattoli, Claudio Sacerdoti Coen, Jui-Hsuan Wu
2025	J	`jnl`	Positive Sharing and Abstract Machines. CoRR Beniamino Accattoli, Claudio Sacerdoti Coen, Jui-Hsuan Wu
2025	B	`conf`	The Cost of Skeletal Call-By-Need, Smoothly. FSCD Beniamino Accattoli, Francesco Magliocca, Loïc Peyrot, Claudio Sacerdoti Coen
2025	J	`jnl`	The Cost of Skeletal Call-by-Need, Smoothly. CoRR Beniamino Accattoli, Francesco Magliocca, Loïc Peyrot, Claudio Sacerdoti Coen
2025	—	`conf`	The Vanilla Sequent Calculus is Call-by-Value. ESOP (1) Beniamino Accattoli
2024	B	`conf`	IMELL Cut Elimination with Linear Overhead. FSCD Beniamino Accattoli, Claudio Sacerdoti Coen
2024	J	`jnl`	IMELL Cut Elimination with Linear Overhead. CoRR Beniamino Accattoli, Claudio Sacerdoti Coen
2024	J	`jnl`	Interaction Equivalence. CoRR Beniamino Accattoli, Adrienne Lancelot, Giulio Manzonetto, Gabriele Vanoni
2024	—	`conf`	Light Genericity. FoSSaCS (2) Beniamino Accattoli, Adrienne Lancelot
2024	B	`conf`	Mirroring Call-By-Need, or Values Acting Silly. FSCD Beniamino Accattoli, Adrienne Lancelot
2024	J	`jnl`	Mirroring Call-by-Need, or Values Acting Silly. CoRR Beniamino Accattoli, Adrienne Lancelot
2024	B	`conf`	Positive Focusing is Directly Useful. MFPS Beniamino Accattoli, Jui-Hsuan Wu
2024	J	`jnl`	Reasonable Space for the λ-Calculus, Logarithmically. Log. Methods Comput. Sci. Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
2024	B	`conf`	Semantic Bounds and Multi Types, Revisited. CSL Beniamino Accattoli
2024	J	`jnl`	The Vanilla Sequent Calculus is Call-by-Value. CoRR Beniamino Accattoli
2023	J	`jnl`	A Diamond Machine For Strong Evaluation. CoRR Beniamino Accattoli, Pablo Barenbaum
2023	B	`conf`	A Diamond Machine for Strong Evaluation. APLAS Beniamino Accattoli, Pablo Barenbaum
2023	J	`jnl`	A Log-Sensitive Encoding of Turing Machines in the λ-Calculus. CoRR Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
2023	J	`jnl`	Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic. Log. Methods Comput. Sci. Beniamino Accattoli
2023	B	`conf`	Formalizing Functions as Processes. ITP Beniamino Accattoli, Horace Blanc, Claudio Sacerdoti Coen
2023	J	`jnl`	Normal Form Bisimulations By Value. CoRR Beniamino Accattoli, Claudia Faggian, Adrienne Lancelot
2023	J	`jnl`	Semantic Bound and Multi Types, Revisited. CoRR Beniamino Accattoli
2023	—	`conf`	Sharing a Perspective on the λ-Calculus. Onward! Beniamino Accattoli
2023	C	`conf`	Strong Call-by-Value and Multi Types. ICTAC Beniamino Accattoli, Giulio Guerrieri, Maico Leberle
2023	J	`jnl`	Strong Call-by-Value and Multi Types. CoRR Beniamino Accattoli, Giulio Guerrieri, Maico Leberle
2022	J	`jnl`	Call-by-Value Solvability and Multi Types. CoRR Beniamino Accattoli, Giulio Guerrieri
2022	A*	`conf`	Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic. LICS Beniamino Accattoli
2022	J	`jnl`	Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic. CoRR Beniamino Accattoli
2022	J	`jnl`	Multi Types and Reasonable Space (Long Version). CoRR Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
2022	J	`jnl`	Multi types and reasonable space. Proc. ACM Program. Lang. Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
2022	A*	`conf`	Reasonable Space for the λ-Calculus, Logarithmically. LICS Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
2022	J	`jnl`	Reasonable Space for the λ-Calculus, Logarithmically. CoRR Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
2022	J	`jnl`	The Theory of Call-by-Value Solvability (long version). CoRR Beniamino Accattoli, Giulio Guerrieri
2022	J	`jnl`	The theory of call-by-value solvability. Proc. ACM Program. Lang. Beniamino Accattoli, Giulio Guerrieri
2022	B	`conf`	Useful Open Call-By-Need. CSL Beniamino Accattoli, Maico Leberle
2021	B	`conf`	Factorize Factorization. CSL Beniamino Accattoli, Claudia Faggian, Giulio Guerrieri
2021	J	`jnl`	Semantic Bounds and Strong Call-by-Value Normalization. CoRR Beniamino Accattoli, Giulio Guerrieri, Maico Leberle
2021	A*	`conf`	Strong Call-by-Value is Reasonable, Implosively. LICS Beniamino Accattoli, Andrea Condoluci, Claudio Sacerdoti Coen
2021	J	`jnl`	Strong Call-by-Value is Reasonable, Implosively. CoRR Beniamino Accattoli, Andrea Condoluci, Claudio Sacerdoti Coen
2021	J	`jnl`	The (In)Efficiency of interaction. Proc. ACM Program. Lang. Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
2021	J	`jnl`	The Space of Interaction (long version). CoRR Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
2021	A*	`conf`	The Space of Interaction. LICS Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
2021	J	`jnl`	Useful Open Call-by-Need. CoRR Beniamino Accattoli, Maico Leberle
2020	J	`jnl`	Factorize Factorization. CoRR Beniamino Accattoli, Claudia Faggian, Giulio Guerrieri
2020	Misc	`conf`	Functional Pearl: The Distributive λ-Calculus. FLOPS Beniamino Accattoli, Alejandro Díaz-Caro
2020	J	`jnl`	Functional Pearl: The Distributive λ-Calculus. CoRR Beniamino Accattoli, Alejandro Díaz-Caro
2020	J	`jnl`	The (In)Efficiency of Interaction. CoRR Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
2020	J	`jnl`	The Abstract Machinery of Interaction (Long Version). CoRR Ugo Dal Lago, Beniamino Accattoli, Gabriele Vanoni
2020	C	`conf`	The Machinery of Interaction. PPDP Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
2020	J	`jnl`	Tight typings and split bounds, fully developed. J. Funct. Program. Beniamino Accattoli, Stéphane Graham-Lengrand, Delia Kesner
2019	B	`conf`	A Fresh Look at the lambda-Calculus (Invited Talk). FSCD Beniamino Accattoli
2019	J	`jnl`	Abstract machines for Open Call-by-Value. Sci. Comput. Program. Beniamino Accattoli, Giulio Guerrieri
2019	C	`conf`	Crumbling Abstract Machines. PPDP Beniamino Accattoli, Andrea Condoluci, Giulio Guerrieri, Claudio Sacerdoti Coen
2019	J	`jnl`	Crumbling Abstract Machines. CoRR Beniamino Accattoli, Andrea Condoluci, Giulio Guerrieri, Claudio Sacerdoti Coen
2019	B	`conf`	Factorization and Normalization, Essentially. APLAS Beniamino Accattoli, Claudia Faggian, Giulio Guerrieri
2019	J	`jnl`	Factorization and Normalization, Essentially. CoRR Beniamino Accattoli, Claudia Faggian, Giulio Guerrieri
2019	—	`ed.`	Proceedings of the 13th Workshop on Logical and Semantic Frameworks with Applications, LSFA 2018, Fortaleza, Brazil, September 26-28, 2018 LSFA Beniamino Accattoli, Carlos Olarte
2019	C	`conf`	Sharing Equality is Linear. PPDP Andrea Condoluci, Beniamino Accattoli, Claudio Sacerdoti Coen
2019	J	`jnl`	Sharing Equality is Linear. CoRR Andrea Condoluci, Beniamino Accattoli, Claudio Sacerdoti Coen
2019	J	`jnl`	Types by Need (Extended Version). CoRR Beniamino Accattoli, Giulio Guerrieri, Maico Leberle
2019	A	`conf`	Types by Need. ESOP Beniamino Accattoli, Giulio Guerrieri, Maico Leberle
2018	—	`conf`	Preface. LSFA Beniamino Accattoli, Carlos Olarte
2018	C	`conf`	Proof Nets and the Linear Substitution Calculus. ICTAC Beniamino Accattoli
2018	J	`jnl`	Proof Nets and the Linear Substitution Calculus. CoRR Beniamino Accattoli
2018	J	`jnl`	Tight Typings and Split Bounds. CoRR Beniamino Accattoli, Stéphane Graham-Lengrand, Delia Kesner
2018	J	`jnl`	Tight typings and split bounds. Proc. ACM Program. Lang. Beniamino Accattoli, Stéphane Graham-Lengrand, Delia Kesner
2018	J	`jnl`	Types of Fireballs (Extended Version). CoRR Beniamino Accattoli, Giulio Guerrieri
2018	B	`conf`	Types of Fireballs. APLAS Beniamino Accattoli, Giulio Guerrieri
2017	—	`conf`	(In)Efficiency and Reasonable Cost Models. LSFA Beniamino Accattoli
2017	J	`jnl`	Encoding Turing Machines into the Deterministic Lambda-Calculus. CoRR Ugo Dal Lago, Beniamino Accattoli
2017	C	`conf`	Environments and the complexity of abstract machines. PPDP Beniamino Accattoli, Bruno Barras
2017	J	`jnl`	Implementing Open Call-by-Value (Extended Version). CoRR Beniamino Accattoli, Giulio Guerrieri
2017	—	`conf`	Implementing Open Call-by-Value. FSEN Beniamino Accattoli, Giulio Guerrieri
2017	J	`jnl`	On the value of variables. Inf. Comput. Beniamino Accattoli, Claudio Sacerdoti Coen
2017	J	`jnl`	The Maximal MAM, a Reasonable Implementation of the Maximal Strategy. CoRR Beniamino Accattoli
2017	B	`conf`	The Negligible and Yet Subtle Cost of Pattern Matching. APLAS Beniamino Accattoli, Bruno Barras
2016	J	`jnl`	(Leftmost-Outermost) Beta Reduction is Invariant, Indeed. Log. Methods Comput. Sci. Beniamino Accattoli, Ugo Dal Lago
2016	J	`jnl`	Open Call-by-Value (Extended Version). CoRR Beniamino Accattoli, Giulio Guerrieri
2016	B	`conf`	Open Call-by-Value. APLAS Beniamino Accattoli, Giulio Guerrieri
2016	—	`conf`	The Complexity of Abstract Machines. WPTE@FSCD Beniamino Accattoli
2016	C	`conf`	The Useful MAM, a Reasonable Implementation of the Strong λ-Calculus. WoLLIC Beniamino Accattoli
2015	B	`conf`	A Strong Distillery. APLAS Beniamino Accattoli, Pablo Barenbaum, Damiano Mazza
2015	J	`jnl`	A Strong Distillery. CoRR Beniamino Accattoli, Pablo Barenbaum, Damiano Mazza
2015	A*	`conf`	On the Relative Usefulness of Fireballs. LICS Beniamino Accattoli, Claudio Sacerdoti Coen
2015	J	`jnl`	On the Relative Usefulness of Fireballs. CoRR Beniamino Accattoli, Claudio Sacerdoti Coen
2015	J	`jnl`	Proof nets and the call-by-value λ-calculus. Theor. Comput. Sci. Beniamino Accattoli
2014	A*	`conf`	A nonstandard standardization theorem. POPL Beniamino Accattoli, Eduardo Bonelli, Delia Kesner, Carlos Lombardi
2014	J	`jnl`	Beta Reduction is Invariant, Indeed (Long Version). CoRR Beniamino Accattoli, Ugo Dal Lago
2014	—	`conf`	Beta reduction is invariant, indeed. CSL-LICS Beniamino Accattoli, Ugo Dal Lago
2014	J	`jnl`	Distilling Abstract Machines (Long Version). CoRR Beniamino Accattoli, Pablo Barenbaum, Damiano Mazza
2014	A	`conf`	Distilling abstract machines. ICFP Beniamino Accattoli, Pablo Barenbaum, Damiano Mazza
2014	C	`conf`	On the Value of Variables. WoLLIC Beniamino Accattoli, Claudio Sacerdoti Coen
2013	A*	`conf`	Compressing Polarized Boxes. LICS Beniamino Accattoli
2013	—	`conf`	Evaluating functions as processes TERMGRAPH Beniamino Accattoli
2013	—	`conf`	Linear Logic and Strong Normalization. RTA Beniamino Accattoli
2012	—	`conf`	An Abstract Factorization Theorem for Explicit Substitutions. RTA Beniamino Accattoli
2012	Misc	`conf`	Call-by-Value Solvability, Revisited. FLOPS Beniamino Accattoli, Luca Paolini
2012	J	`jnl`	On the Invariance of the Unitary Cost Model for Head Reduction (Long Version) CoRR Beniamino Accattoli, Ugo Dal Lago
2012	—	`conf`	On the Invariance of the Unitary Cost Model for Head Reduction. RTA Beniamino Accattoli, Ugo Dal Lago
2012	J	`jnl`	Preservation of Strong Normalisation modulo permutations for the structural lambda-calculus Log. Methods Comput. Sci. Beniamino Accattoli, Delia Kesner
2012	B	`conf`	Proof Pearl: Abella Formalization of λ-Calculus Cube Property. CPP Beniamino Accattoli
2012	—	`conf`	Proof nets and the call-by-value lambda-calculus LSFA Beniamino Accattoli
2012	B	`conf`	The Permutative λ-Calculus. LPAR Beniamino Accattoli, Delia Kesner
2010	B	`conf`	The Structural CSL Beniamino Accattoli, Delia Kesner
2009	B	`conf`	Jumping Boxes. CSL Beniamino Accattoli, Stefano Guerrini