Investigador Asistente – CONICET / UNQ / ICC.
Profesor Adjunto – DC, FCEyN, UBA.
I am a member of the LoReL team, the Logics and Dynamics of Programming Languages Group of the LIA SINFIN, and the FunLeP group. In 2020, I defended my PhD in Computer Science at DC, FCEyN, UBA. My advisors were Eduardo Bonelli and Delia Kesner. The main topic of my thesis was evaluation strategies in calculi of explicit substitutions at a distance. Most of my PhD was funded by a CONICET grant.
My research interests gravitate towards the lambda calculus and its various manifestations, including rewriting theory, type theory, proof theory, and the foundations and implementation of programming languages and proof-assistants.
Publications
- PB, Delia Kesner, Mariana Milicich. A Fresh Inductive Approach to Useful Call-by-Value. CADE 2025.
- PB, Simona Ronchi Della Rocca, Cristian Sottile. Strong normalization through idempotent intersection types: a new syntactical approach. MFPS 2025.
- PB, Eduardo Bonelli. Sharing and Linear Logic with Restricted Access. FoSSaCs 2025. [pdf] [arXiv] (ETAPS best paper)
- PB, Delia Kesner, Mariana Milicich. Hybrid Intersection Types for PCF. LPAR 2024. [pdf] [arXiv]
- Beniamino Accattoli, PB. A Diamond Machine for Strong Evaluation. APLAS 2023. [arXiv]
- PB, Cristian Sottile. Two Decreasing Measures for Simply Typed λ-Terms. FSCD 2023. [pdf] [arXiv]
- PB, Eduardo Bonelli. Reductions in Higher-Order Rewriting and Their Equivalence. CSL 2023. [pdf] [arXiv]
- PB, Teodoro Freund. Proofs and Refutations for Intuitionistic and Second-Order Logic. CSL 2023. [pdf] [arXiv]
- PB, Teodoro Freund. A Constructive Logic with Classical Proofs and Refutations. LICS 2021. [pdf] [arXiv]
- PB, Federico Lochbaum, Mariana Milicich. Semantics of a Relational λ-calculus. ICTAC 2020. [pdf] [arXiv]
- PB, Eduardo Bonelli. Rewrites as Terms through Justification Logic. PPDP 2020. [pdf]
- PB, Gonzalo Ciruelos. Factoring Derivation Spaces via Intersection Types. APLAS 2018. [pdf] [arXiv]
- PB, Eduardo Bonelli, Kareem Mohamed. Pattern Matching and Fixed Points: Resource Types and Strong Call-By-Need. PPDP 2018: 6:1-6:12. [pdf]
- PB, Eduardo Bonelli. Optimality and the Linear Substitution Calculus. FSCD 2017: 9:1-9:16. [pdf]
- Thibaut Balabonski, PB, Eduardo Bonelli, Delia Kesner. Foundations of Strong Call-by-Need. ICFP 2017: 20:1-20:29. [pdf]
- Beniamino Accattoli, PB, Damiano Mazza. A Strong Distillery. APLAS 2015: 231-250. [pdf] [arXiv]
- Beniamino Accattoli, PB, Damiano Mazza. Distilling Abstract Machines. ICFP 2014: 363-376. [pdf] [arXiv]
- PB, Verónica Becher, Alejandro Deymonnaz, Melisa Halsband, Pablo Ariel Heiber. Efficient repeat finding in sets of strings via suffix arrays. DMTCS 15(2): 59-70 (2013). [pdf]
Thesis manuscripts
- PhD Thesis: Semántica dinámica de cálculos de sustituciones explícitas a distancia, Departamento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires, 2020 [pdf] (unofficial English manuscript).
- Master Thesis: Superdevelopments en el Cálculo-Lambda Débil, 2010 [pdf] (in Spanish).
PhD Students
- 2024-02-01: Leopoldo Lerena started a PhD at UBA. Topic: calculi for classical and linear logic.
- 2022-10-01: Mariana Milicich started a PhD, jointly between UBA and UPC, with Delia Kesner as a co-supervisor, financed by a FSMP scholarship. Topic: Quantitative Types for Higher-Order Programming Languages.
Master's Students
- Ongoing – Julia Zanette (UBA), expansive models of type theory via idempotent operators.
- Ongoing – Rocío Casco (UBA), a symmetric lambda-calculus with a classical modality.
- Ongoing – Leandro Lovisolo (UBA), an empiric measure of partial evaluation based on interaction.
- Ongoing – Francisco Giordano (UBA), abstract machines for functional–logic programming.
- 2024-12-23 Manuel Panichelli (UBA), defended his Master's thesis in Computer Science: PPA – Un asistente de demostración para lógica de primer orden con extracción de testigos usando la traducción de Friedman.
- 2024-02-21 Giselle Zeitoune (UBA) defended her Master's thesis in Computer Science: Un cálculo-λ cronometrado.
- 2022-08-10 Mariana Milicich (UBA) defended her Master's thesis in Computer Science: Semántica denotacional para un cálculo-λ relacional.
- 2021-11-05 – Teodoro Freund (UBA) defended his Master's thesis in Computer Science: PRK, una lógica constructiva clásica.
- 2021-04-20 – Federico Lochbaum (UNQ) defended his Master's thesis: Fundamentos e implementación de un lenguaje funcional–lógico.
- 2018-06-28 – Gonzalo Ciruelos (UBA) defended his Master's thesis in Computer Science: Factorización de derivaciones a través de tipos intersección [pdf].
Events
- 12th International Workshop on Higher Order Rewriting (HOR 2025). Birmingham, United Kingdom. 14th July, 2025.
Talks
- 2024-12: A MELL calculus based on contraposition [slides] – Irif, Université Paris Cité.
- 2023-11: Sharing in Linear Logic and Call-by-Need [slides] – Irif, Université Paris Cité.
- 2023-07: Proof Terms for Higher-Order Rewriting and Their Equivalence – LSFA 2023 (Invited Talk), Università di Roma.
- 2023-07: Quantitative Types for Useful Reduction [slides] – HOR 2023 (Invited Talk), Università di Roma.
- 2023-05: Una lógica constructiva con pruebas y refutaciones clásicas [slides] – 3er encuentro FunLeP (Córdoba).
- 2023-02: Proof Terms for Higher-Order Rewriting and Their Equivalence [slides] – CSL 2023, University of Warsaw.
- 2023-02: Proofs and Refutations for Intuitionistic and Second-Order Logic [slides] – CSL 2023, University of Warsaw.
- 2022-10: Proof Terms for Higher-Order Rewriting and Their Equivalence [slides] – Irif, Université Paris Cité.
- 2022-08: Demostraciones ejecutables [slides] – Ciclo de charlas Ciencias de la Computación, Café y Chocolate, Instituto de Ciencias de la Computación, Universidad de Buenos Aires.
- 2022-03: A Constructive Logic with Classical Proofs and Refutations [slides] – French-Argentinian Workshop on Logics and Dynamics of Programming Languages, Irif, Université Paris Cité.
- 2021-06: A Constructive Logic with Classical Proofs and Refutations [slides] – LICS 2021.
- 2020-11: Semantics of a Relational λ-Calculus [slides] – ICTAC 2020.
- 2020-11: PhD thesis defense [slides].
- 2020-06: A relational λ-calculus [slides] – weekly seminar of the LoReL group.
- 2018-12: Factoring Derivation Spaces via Intersection Types [slides] – APLAS 2018, Victoria University of Wellington, New Zealand.
- 2018-08: Pattern Matching and Fixed Points: Resource Types and Strong Call-By-Need [slides] – PPDP 2018, Goethe-Universität, Frankfurt, Germany.
- 2018-05: Factoring Derivation Spaces via Intersection Types [slides] – Logic and Foundations of Programming Languages Day, Universidad de Buenos Aires.
- 2017-10: Foundations of Strong Call-by-Need [slides] – INFINIS Seminar, Universidad de Buenos Aires.
- 2017-09: Optimality and the Linear Substitution Calculus [slides] – FSCD'17, University of Oxford.
- 2016-10: Finite Family Developments for the Linear Substitution Calculus [slides] – Semantics Seminar, Irif, Université Paris 7.
- 2014-05: Optimal Reduction in the Linear Substitution Calculus [slides] – LoReL seminar, Departamento de Computación, Universidad de Buenos Aires.
Profesor Adjunto –
DC,
FCEyN,
UBA.
The following table summarizes the subjects in which I have been involved:
| Semester | UBA | UNQ |
|---|---|---|
| 2025(1) | PAdj – PLP | |
| 2024(2) | PAdj – PLP | PI – PyGC |
| 2024(1) | PAdj – PLP | PI – TC |
| 2023(2) | PAdj – PLP, RCLyT | PI – PyGC |
| 2023(1) | PAdj – PLP | PI – TC |
| 2022(2) | JTP – AyED2 | PI – PyGC |
| 2022(1) | JTP – AyED1 | PI – TC |
| 2021(2) | JTP – AyED1 | PI – PyGC |
| 2021(1) | JTP – AyED1 | PI – TC |
| 2020(2) | JTP – AyED2 | PI – PyGC |
| 2020(1) | JTP – AyED2 | PI – ED |
| 2019(2) | JTP – AyED2 | PI – PyGC |
| 2019(1) | JTP – AyED2 | PI – ED |
| 2018(2) | JTP – AyED2 | PI – PyGC |
| 2018(1) | JTP – AyED2 | PI – ED |
| 2017(2) | PI – PyGC | |
| 2017(1) | PI – ED | |
| 2016(2) | PI – PyGC | |
| 2016(1) | PI – InPr | |
| 2015(2) | PI – InPr | |
| 2015(1) | PI – InPr | |
| 2014(2) | JTP – AyED2 | PI – InPr |
| 2014(1) | JTP – PLP | PI – InPr |
| 2013(2) | PI – InPr | |
| 2013(1) | JTP – AyED2 | PI – InPr |
| 2012(2) | Ay1 – PLP | PI – InPr |
| 2012(1) | Ay1 – AyED2 | PI – InPr |
| 2011(2) | Ay1 – PLP | PI – InPr |
| 2011(1) | Ay1 – PLP | PI – InPr |
| 2010(2) | Ay2 – PLP | |
| 2010(1) | Ay2 – PLP | |
| 2009(2) | Ay2 – PLP | |
| 2009(1) | Ay2 – PLP | |
| 2008(2) | Ay1 – PLP | |
| 2008(1) | Ay2 – AyED2 | |
| 2007(2) | Ay2 – PLP | |
| 2007(1) | Ay2 – AyED2 | |
| 2006(2) | Ay2 – AyED2 | |
| 2006(1) | Ay2 – AyED2 |
Key
Positions
Ay2: Ayudante de Segunda.
Ay1: Ayudante de Primera.
JTP: Jefe de Trabajos Prácticos.
PI: Profesor Instructor.
PAdj: Profesor Adjunto.
Subjects
AyED1: Algoritmos y Estructuras de Datos 1.
AyED2: Algoritmos y Estructuras de Datos 2.
ED: Estructuras de Datos.
InPr: Introducción a la Programación.
PyGC: Parseo y Generación de Código.
PLP: Paradigmas de Lenguajes de Programación.
RCLyT: Reescritura, Cálculo-Lambda y Tipos.
TC: Teoría de la Computación.
- Materias
- Lenguajes de programación
- PyGobstones (2011–2012)
- Gobstones Web (2017–2018)
- Qriollo
- Cómo rompe las palabras – Color Ámbar
- El cubo negro
- YouTube
- Amadorenbaum company memorial
- Labandalambda
- Misc2
- My sister is a musician.