Cristian Sottile

I am an Assistant Professor at UNQ, where I am a member of the Logic and Rewriting for Programming Languages (LoReL) team, and currently I am also a Visiting Researcher at IRIF, where I am a member of the Proofs, Programs and Systems (PPS) pole. I work mostly on termination proofs of typed lambda calculi, and during my visit at IRIF I will work on non-idempotent intersection types with Delia Kesner and Giulio Manzonetto.

Current Position

Visiting Researcher @ Institut de Recherche en Informatique Fondamentale

Assistant Professor @ Universidad Nacional de Quilmes

Education

• PhD in Computer Science @ Universidad de Buenos Aires (DC-Exactas)
  Thesis: Strong normalization proof strategies in typed lambda-calculi: New decreasing measures [PDF]
  Director: Alejandro Díaz-Caro. Co-director: Pablo E. "Fidel" Martínez López.
• MSc. in Informatics @ Universidad Nacional de La Plata (FInfo)
  Thesis: Adding polymorphism to a logic identifying isomorphic propositions [SEDICI-UNLP]

Publications

• A formalization of System I with type Top in Agda arXiv
  A. Séttimo, C. Sottile, C. Manzino. IFL '25. 2026.
• Strong normalization through idempotent intersection types: a new syntactical approach ENTICS 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.

Teaching

• Programming Language Foundations (2026, 2025, 2024, 2023, 2022) Curriculum
• Logic and Programming (2026, 2025, 2022) Curriculum
• Data Structures (2024, 2023, 2022, 2021, 2020, 2019) Curriculum
• Functional Programming (2020, 2019, 2018, 2017) Curriculum
• Introduction to Programming (2018) Curriculum

Students

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

Presentations

• Strong normalization proof strategies in typed lambda-calculi YouTube Slides
  PhD defence. Departamento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires. July 3, 2026.
• 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.