Current Position
PhD Student (CONICET Doctoral Fellow) @ ICC (UBA/CONICET)
I am a member of the LoReL (Logic and Rewriting for Programming Languages) team. I work in the elaboration of new techniques for proving termination of programs (strong normalization) in different variants of typed lambda calculus. Previously, I worked in the design of programming languages equating isomorphic types.
Director: Alejandro Díaz-Caro
Co-director: Pablo E. "Fidel" Martínez López.
Head Teaching Assistant @ UNQ (CPI)
Taught courses: Foundations of Programming Languages, Logic, Data Structures, Functional Programming, Introduction to Programming.
Education
- Pursuing PhD in Computer Science @ UBA (DC-Exactas)
-
MSc. in
Informatics @ UNLP (FInfo)
Thesis: Adding polymorphism to a logic identifying isomorphic propositions [SEDICI-UNLP]
Publications
-
Strong normalization through idempotent intersection types: a
new syntactical approach
Pre–proceedings
arXiv
P. Barenbaum, S. Ronchi Della Rocca, C. Sottile. MFPS '25. 2025
-
Two decreasing measures for Simply Typed Lambda-Terms
LIPIcs
arXiv
P. Barenbaum, C. Sottile. FSCD '23. 2023
-
Polymorphic System I
ACM
arXiv
Erratum
There is an unintended error in the Strong Normalization proof presented in the published version. Although we conjecture that the theorem is valid, the current proof is incorrect and we are working in a correct proof.C. Sottile, A. Díaz-Caro, P. E. Martínez López. IFL '20. 2021.
Students
Presentations
-
Una medida decreciente directa para tipos intersección
Slides
6th JIF (Meeting of Early Career Researchers in Science and Technology). Universidad Nacional de Quilmes. November 14, 2025.
-
Reducibility candidates modulo isomorphisms
Slides
37th Symposium on Implementation and Application of Functional Languages. Universidad de la República. Uruguay. October 3, 2025.
-
Termination guarantees in polymorphic lambda calculi
Slides
Poster
7th Day of Instituto de Investigación en Ciencias de la Computación. Universidad de Buenos Aires. August 14, 2025.
-
Strong normalization and decreasing measures: syntactic proofs
of termination in typed lambda calculus
Slides
54 JAIIO. Universidad de Buenos Aires. August 4, 2025.
-
Strong normalization through idempotent intersection types: a
new syntactical approach
Slides
Proofs & Algorithms Seminar. École Polytechnique, Paris. June 30, 2025.
-
Strong normalization through idempotent intersection types: a
new syntactical approach
YouTube
Slides
41st Conference on Mathematical Foundations of Programming Semantics MFPS XLI. University of Strathclyde, Glasgow. June 20, 2025.
-
Strong normalization and decreasing measures: syntactic proofs
of termination in typed lambda calculus
YouTube
Slides
XXII Jornadas de Ciencias de la Computación. DCC, FCEIA, Universidad Nacional de Rosario. October 25, 2024.
-
A syntactic approach to Strong Normalization through decreasing
measures
Slides
20th Latin American Symposium on Mathematical Logic. Universidad de la República, Uruguay. July 2, 2024.
-
Measuring programs to prove termination
Slides
5th JIF (Meeting of Early Career Researchers in Science and Technology). Universidad Nacional de Quilmes. September 28, 2023.
-
Two decreasing measures for STLC
Slides
8th International Conference on Formal Structures for Computation and Deduction. Sapienza Università di Roma. July 5, 2023.
-
Two decreasing measures for STLC
Slides
3rd FunLeP (Programming Language Foundations) Meeting. Universidad Nacional de Córdoba. May 18, 2023.
-
Measuring programs to prove they terminate
Slides
5th Day of Instituto de Investigación en Ciencias de la Computación. Universidad de Buenos Aires. March 28, 2023.
-
Strong normalisation in a System F modulo isomorphisms
Deducteam Seminar. Deducteam, Laboratoire Méthodes Formelles, Université Paris-Saclay. October 6, 2022.
-
Quotienting programs by final utility
Slides
4th Day of Instituto de Investigación en Ciencias de la Computación. Universidad de Buenos Aires. March 18, 2022.
-
Adding polymorphism to a logic identifying isomorphic
propositions (Masters thesis abstract)
YouTube
XXIV Concurso de Trabajos Estudiantiles (EST 2021) - JAIIO 50. INTA (Virtual). October 29, 2021.
-
Equating polymorphic programs with the same final utility
YouTube
4th JIF (Meeting of Early Career Researchers in Science and Technology). Universidad Nacional de Quilmes. March 25, 2021.
-
Towards a practical implementation of programming languages
equating isomorphic types
YouTube
IV Jornadas de Investigadores en Formación. Universidad Nacional de Quilmes. March 25, 2021.
-
Polymorphic System I
YouTube
32nd Symposium on Implementation and Application of Functional Languages. University of Kent. September 4, 2020.
-
Communication talk
YouTube
Computer Science Week (Stay at home). Universidad de Buenos Aires. September 2, 2020.