Elif Üsküplü

Since August 2024, I have been a Zorn’s Postdoctoral Fellow at Indiana University, Bloomington, under the supervision of Prof. Larry Moss. I was a lecturer in the Department of Mathematics at the University of Southern California in the Spring 24 semester. In March–April 2027, I will be a research member of the program AxIOM: Building the Mathematical Library of the Future at SLMath, Berkeley.

My research interests span logic, foundations of mathematics, category theory, homotopy type theory, and natural logic. I am also interested in formalization of mathematics and the ethical use of AI in mathematics and education. My secondary research interests include combinatorial design theory and coding theory.

I received my Ph.D from USC with the thesis named Formalizing two-level type theory with cofibrant exo-nat. I am studying on homotopy type theory, and my thesis advisors are Prof. Aaron Lauda and Prof. Michael Shulman.

I have been awarded the Edward and Dolores Blum Research Prize by the USC Graduate Committee. More recently, I received the Max Zorn Teaching Award from the Department of Mathematics at Indiana University in recognition of excellence in teaching.

I earned my M.Sc. degree from Koç University in 2019, with the thesis “LDPC codes from partially balanced incomplete block designs”, under the supervision of Prof. Emine Şule Yazıcı. I earned my B.Sc. degree from Bilgi University in 2017 with the project “The Game Of Hex & The Brouwer Fixed Point Theorem”, under the supervision of Kemal Ilgar Eroğlu.

Publications

7) Prolegomena to semantic and algorithmic treatments of polarity tagging - Lawrence S. Moss, Elif Uskuplu - Book chapter, to appear in an edited volume.

6) Formalizing the Bruck–Ryser–Chowla Theorem: Combinatorial Design Theory in Lean - Eric Jonathan Wang, Elif Uskuplu - 17th International Conference on Interactive Theorem Proving (ITP 2026) - Leibniz International Proceedings in Informatics (LIPIcs), vol. 382 , July 2026.

5) FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified? - Nikil Ravi, Kexing Ying, Vasilii Nesterov, Rayan Krishnan, Elif Uskuplu, Bingyu Xia, Janitha Aswedige, Langston Nashold - ICLR 2026 Workshop VerifAI-2 - Mar 2026.

4) KnowTeX: Visualizing Mathematical Dependencies - Elif Uskuplu, Lawrence S. Moss, Valeria de Paiva - arXiv preprint - Dec 2025.

3) Formalizing two-level type theory with cofibrant exo-nat - Elif Uskuplu - Mathematical Structures in Computer Science - vol. 35, p. e30 - Nov 2025.

2) QC-LDPC Codes from Difference Matrices and Difference Covering Arrays - Diane Donovan, Asha Rao, Elif Üsküplü, Emine Ş.Yazıcı - in IEEE Access, vol. 11, pp. 52141-52157 - Jun 2023.

1) High-rate LDPC codes from partially balanced incomplete block designs - Diane Donovan, Aiden Price, Asha Rao, Elif Üsküplü, Emine Ş.Yazıcı - Journal of Algebraic Combinatorics - Jan 2022.

In Preparation

2) A Semantic Treatment of Polarity Tagging - Lawrence S. Moss, Elif Uskuplu

1) An Algorithmic Treatment of Polarity Tagging - Elif Uskuplu, Lawrence S. Moss

Conference Abstracts

5) Enhancing Dependency Graphs for Research and Alignment in Math - Valeria de Paiva, Lawrence S. Moss, Elif Uskuplu - ALIGN 2025: Math Datasets and Libraries: Alignments and Comparisons - 2025

4) From parametricity to identity types - Thorsten Altenkirch, Ambrus Kaposi, Michael Shulman, Elif Uskuplu - TYPES 2025: 31st International Conference on Types for Proofs and Programs - 2025

3) Internal relational parametricity, without an interval - Thorsten Altenkirch, Ambrus Kaposi, Michael Shulman, Elif Uskuplu - TYPES 2024: 30th International Conference on Types for Proofs and Programs - 2024

2) Cofibrancy of the exo-type of natural numbers - Elif Uskuplu - HoTT 2023: Second International Conference on Homotopy Type Theory - 2023

1) An experiment with 2LTT features in Agda - Elif Uskuplu - HoTT/UF 2022: Workshop on Homotopy Type Theory/Univalent Foundations - 2022

Service

4) Program Committee Member - LSFA 2026: Logical and Semantic Frameworks with Applications - 2026

3) Referee - Forum of Mathematics, Sigma - 2025

2) Reviewer - COLING 2025: The 31st International Conference on Computational Linguistics - 2025

1) Research Event Coordinator - USC Women in Mathematics - 2022–2023

Talks

11) “Enhancing Dependency Graphs for Research and Alignment in Math” - The Workshop on Math Datasets: Alignments and Comparisons (Align 2025) - Oct 10 2025

10) “Monotonicity and Natural Logic: Tracking Meaning with Arrows” - AWM Research Symposium, Logic Across Mathematics Session - May 17 2025

9) “Formalizing locally nameless syntax with cofinite quantification” - WITS’ 25 - Jan 25 2025

8) “From Propositions to Proof Assistants: A Journey through Type Theory” - IUB Logic Seminars - Sep 25 & Oct 2, 2024

7) “Navigating the New Frontier: Formalized Mathematics” - WiMSoCal 2024 - Feb 2024.

6) “Cofibrancy of The Exo-type of Natural Numbers” - The Second International Conference on Homotopy Type Theory - May 2023.

5) “Homotopy Type Theory vs Set Theory” - GSU Research Seminars - December 2022.

4) “Proof Assistants: Agda for Beginners” - Sagedays Istanbul - August 2022.

3) “An Experiment with 2LTT Features in Agda” - Workshop on Homotopy Type Theory/ Univalent Foundations - July 31 - August 1, 2022.

2) “Formalization of 2LTT in Agda” - MURI Meeting at CMU - July 2022. Slide

1) “A brief Introduction to Homotopy Type Theory” - USC Math Grad Colloquium - February 2022.

Notes

2) Simplicial Sets & Complete Segal Spaces: A Visual and Interactive Library Link

1) Documentation for the two-level flag in Agda Library Link

Projects

7) KnowTeX: Visualizing Mathematical Dependencies, Available on Github. Try it here.

6) Narya: A proof assistant for higher-dimensional type theory (as a contributor), Available on Github.

5) PrimeNumberTheoremAnd: Formalization of the Prime Number Theorem in Lean4 (as a contributor), Available on Github.

4) Combinatorial Designs Formalization in Lean4, with Eric Jonathan Wang, Available on Github.

3) Formalization of 2LTT & Univalence Principle in Agda - Available on Github.

2) Univalent mathematics in Agda (as a maintainer) - Available on Github.

1) Simply Typed Lambda Calculus with de Bruijn Indices in Lean4 - Available on Github.