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
- Pablo Barenbaum, Cristian Sottile. Two Decreasing Measures for Simply Typed λ-Terms. FSCD 2023. [pdf] [arXiv]
- Pablo Barenbaum, Eduardo Bonelli. Reductions in Higher-Order Rewriting and Their Equivalence. CSL 2023. [pdf] [arXiv]
- Pablo Barenbaum, Teodoro Freund. Proofs and Refutations for Intuitionistic and Second-Order Logic. CSL 2023. [pdf] [arXiv]
- Pablo Barenbaum, Teodoro Freund. A Constructive Logic with Classical Proofs and Refutations. LICS 2021. [pdf] [arXiv]
- Pablo Barenbaum, Federico Lochbaum, Mariana Milicich. Semantics of a Relational λ-calculus. ICTAC 2020. [pdf] [arXiv]
- Pablo Barenbaum, Eduardo Bonelli. Rewrites as Terms through Justification Logic. PPDP 2020. [pdf]
- Pablo Barenbaum, Gonzalo Ciruelos. Factoring Derivation Spaces via Intersection Types. APLAS 2018. [pdf] [arXiv]
- Pablo Barenbaum, Eduardo Bonelli, Kareem Mohamed. Pattern Matching and Fixed Points: Resource Types and Strong Call-By-Need. PPDP 2018: 6:1-6:12. [pdf]
- Pablo Barenbaum, Eduardo Bonelli. Optimality and the Linear Substitution Calculus. FSCD 2017: 9:1-9:16. [pdf]
- Thibaut Balabonski, Pablo Barenbaum, Eduardo Bonelli, Delia Kesner. Foundations of Strong Call-by-Need. ICFP 2017: 20:1-20:29. [pdf]
- Beniamino Accattoli, Pablo Barenbaum, Damiano Mazza. A Strong Distillery. APLAS 2015: 231-250. [pdf] [arXiv]
- Beniamino Accattoli, Pablo Barenbaum, Damiano Mazza. Distilling Abstract Machines. ICFP 2014: 363-376. [pdf] [arXiv]
- Pablo Barenbaum, 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 – Werner Busch (UBA), notions of finity and infinity in constructive type theory.
- Ongoing – Manuel Panichelli (UBA), a Mizar-like proof-checker for classical first-order logic with witness extraction based on Friedman's translation.
- Ongoing – Leandro Lovisolo (UBA), an empiric measure of partial evaluation based on interaction.
- Ongoing – Francisco Giordano (UBA), abstract machines for functional–logic programming.
- 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].
Talks
- 2023-11: Sharing in Linear Logic and Call-by-Need [slides] – Irif.
- 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.
Profesor Instructor –
UNQ.
The following table summarizes the subjects in which I have been involved:
| Semester | UBA | UNQ |
|---|---|---|
| 2024(1) | PAdj – PLP | PI – TC |
| 2023(2) | PAdj – PLP | PI – PGC |
| 2023(1) | PAdj – PLP | PI – TC |
| 2022(2) | JTP – AyED2 | PI – PGC |
| 2022(1) | JTP – AyED1 | PI – TC |
| 2021(2) | JTP – AyED1 | PI – PGC |
| 2021(1) | JTP – AyED1 | PI – TC |
| 2020(2) | JTP – AyED2 | PI – PGC |
| 2020(1) | JTP – AyED2 | PI – ED |
| 2019(2) | JTP – AyED2 | PI – PGC |
| 2019(1) | JTP – AyED2 | PI – ED |
| 2018(2) | JTP – AyED2 | PI – PGC |
| 2018(1) | JTP – AyED2 | PI – ED |
| 2017(2) | PI – PGC | |
| 2017(1) | PI – ED | |
| 2016(2) | PI – PGC | |
| 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.
PGC: Parseo y Generación de Código.
PLP: Paradigmas de Lenguajes de Programación.
TC: Teoría de la Computación.
Software
I have been involved in the development of PyGobstones (2011–2012) and Gobstones Web (2017–2018). These are free software tools that implement the Gobstones programming language.
The Gobstones programming language was designed by a group of researchers and teachers at the University of Quilmes, lead by Pablo "Fidel" Martínez López, to teach students without any previous exposure to programming.
Reading group
In 2014 and during 2016–2021, I coordinated an informal weekly reading group on the lambda-calculus.