Cristian Sottile

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]
  C. Sottile, A. Díaz-Caro, P. E. Martínez López. IFL '20. 2021

Students

• A formalization of System I with Top [Github]
  Agustín Settimo's MSc. in Computer Science thesis. Director: Cecilia Manzino. Codirector: Cristian Sottile. 2024

Presentations

• 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.