Using Fields and Explicit Substitutions to Implement Objects and Functions in a de Bruijn Setting. - Eduardo Bonelli (CSL, 1999)

A de Bruijn Notation for Higher-Order Rewriting. - Eduardo Bonelli; Delia Kesner; Alejandro Ríos 001 (RTA, 2000)

From Higher-Order to First-Order Rewriting. - Eduardo Bonelli; Delia Kesner; Alejandro Ríos 001 (RTA, 2001)

Perpetuality in a named lambda calculus with explicit substitutions. - Eduardo Bonelli (Math. Struct. Comput. Sci., 2001)

A Normalisation Result for Higher-Order Calculi with Explicit Substitutions. - Eduardo Bonelli (FoSSaCS, 2003)

Typechecking Safe Process Synchronization. - Eduardo Bonelli; Adriana B. Compagnoni; Elsa L. Gunter (FGUC, 2004)

Information Flow Analysis for a Typed Assembly Language with Polymorphic Stacks. - Eduardo Bonelli; Adriana B. Compagnoni; Ricardo H. Medel (CASSIS, 2005)

A Typed Assembly Language for Non-interference. - Ricardo H. Medel; Adriana B. Compagnoni; Eduardo Bonelli (ICTCS, 2005)

Correspondence assertions for process synchronization in concurrent communications. - Eduardo Bonelli; Adriana B. Compagnoni; Elsa L. Gunter (J. Funct. Program., 2005)

de Bruijn Indices for Metaterms. - Eduardo Bonelli; Delia Kesner; Alejandro Ríos 001 (J. Log. Comput., 2005)

Relating Higher-order and First-order Rewriting. - Eduardo Bonelli; Delia Kesner; Alejandro Ríos 001 (J. Log. Comput., 2005)

Normalisation for higher-order calculi with explicit substitutions. - Eduardo Bonelli (Theor. Comput. Sci., 2005)

The Linear Logical Abstract Machine. - Eduardo Bonelli (MFPS, 2006)

The Intensional Lambda Calculus. - Sergei N. Artëmov; Eduardo Bonelli (LFCS, 2007)

Multipoint Session Types for a Distributed Calculus. - Eduardo Bonelli; Adriana B. Compagnoni (TGC, 2007)

Boxed ambients with communication interfaces. - Pablo Garralda; Eduardo Bonelli; Adriana B. Compagnoni; Mariangiola Dezani-Ciancaglini (Math. Struct. Comput. Sci., 2007)

Type-based information flow analysis for bytecode languages with variable object field policies. - Francisco Bavera; Eduardo Bonelli (SAC, 2008)

The Logic of Proofs as a Foundation for Certifying Mobile Computation. - Eduardo Bonelli; Federico Feller (LFCS, 2009)

Superdevelopments for Weak Reduction - Eduardo Bonelli; Pablo Barenbaum (WRS, 2009)

Justification Logic and History Based Computation. - Francisco Bavera; Eduardo Bonelli (ICTAC, 2010)

On-the-Fly Inlining of Dynamic Dependency Monitors for Secure Information Flow. - Luciano Bello; Eduardo Bonelli (Formal Aspects in Security and Trust, 2011)

Normalisation for Dynamic Pattern Calculi. - Eduardo Bonelli; Delia Kesner; Carlos Lombardi; Alejandro Ríos 001 (RTA, 2012)

Justification Logic as a foundation for certifying mobile computation. - Eduardo Bonelli; Federico Feller (Ann. Pure Appl. Log., 2012)

BioScape: A Modeling and Simulation Language for Bacteria-Materials Interactions. - Adriana B. Compagnoni; Vishakha Sharma 001; Yifei Bao; Matthew Libera; Svetlana Sukhishvili; Philippe Bidinger; Livio Bioglio; Eduardo Bonelli (CS2Bio, 2012)

Intuitionistic Hypothetical Logic of Proofs. - Gabriela Steren; Eduardo Bonelli (IMLA@UNILOG, 2013)

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

An abstract normalisation result with applications to non-sequential calculi. - Eduardo Bonelli; Delia Kesner; Carlos Lombardi; Alejandro Ríos 001 (CoRR, 2014)

Hypothetical Logic of Proofs. - Eduardo Bonelli; Gabriela Steren (Logica Universalis, 2014)

Efficient Type Checking for Path Polymorphism. - Juan Edi; Andrés Viso; Eduardo Bonelli (TYPES, 2015)

Type Soundness for Path Polymorphism. - Andrés Viso; Eduardo Bonelli; Mauricio Ayala-Rincón (LSFA, 2015)

Optimality and the Linear Substitution Calculus. - Pablo Barenbaum; Eduardo Bonelli (FSCD, 2017)

The first-order hypothetical logic of proofs. - Gabriela Steren; Eduardo Bonelli (J. Log. Comput., 2017)

Foundations of strong call by need. - Thibaut Balabonski; Pablo Barenbaum; Eduardo Bonelli; Delia Kesner (Proc. ACM Program. Lang., 2017)

On abstract normalisation beyond neededness. - Eduardo Bonelli; Delia Kesner; Carlos Lombardi; Alejandro Ríos 001 (Theor. Comput. Sci., 2017)

Pattern Matching and Fixed Points: Resource Types and Strong Call-By-Need: Extended Abstract. - Pablo Barenbaum; Eduardo Bonelli; Kareem Mohamed (PPDP, 2018)

Justification logic and audited computation. - Francisco Bavera; Eduardo Bonelli (J. Log. Comput., 2018)

Strong Bisimulation for Control Operators. - Eduardo Bonelli; Delia Kesner; Andrés Viso (CoRR, 2019)

Typed path polymorphism. - Mauricio Ayala-Rincón; Eduardo Bonelli; Juan Edi; Andrés Viso (Theor. Comput. Sci., 2019)

Strong Bisimulation for Control Operators (Invited Talk). - Delia Kesner; Eduardo Bonelli; Andrés Viso (CSL, 2020)

Rewrites as Terms through Justification Logic. - Pablo Barenbaum; Eduardo Bonelli (PPDP, 2020)

A Strong Bisimulation for Control Operators by Means of Multiplicative and Exponential Reduction. - Eduardo Bonelli; Delia Kesner; Andrés Viso (CoRR, 2021)

Reductions in Higher-Order Rewriting and Their Equivalence. - Pablo Barenbaum; Eduardo Bonelli (CSL, 2023)

A Strong Bisimulation for a Classical Term Calculus. - Eduardo Bonelli; Delia Kesner; Andrés Viso (Log. Methods Comput. Sci., 2024)

Sharing and Linear Logic with Restricted Access. - Pablo Barenbaum; Eduardo Bonelli (FoSSaCS, 2025)

Sharing and Linear Logic with Restricted Access (Extended Version). - Pablo Barenbaum; Eduardo Bonelli (CoRR, 2025)