I am a PhD student in the FP Lab at the University of Nottingham, under the supervision of Nicolai Kraus and co-supervised by Tom de Jong. I am interested in homotopy type theory, higher category theory, and constructive mathematics. My favourite proof assistant is Cubical Agda.
Before coming to Nottingham, I completed an M.Sc in pure mathematics at Sharif University of Technology. Prior to that, I earned a B.Sc in mathematics with a minor in philosophy of science, also at Sharif University.
You’re welcome to contact me:
Email: aref.mohammadzadeh[at]nottingham.ac.uk
Email: arefmohammadzadeh.ac[at]gmail.com
Office: Room C43, School of Computer Science, University of Nottingham, Jubilee Campus, Nottingham NG81BB, United Kingdom.
Dec 2025: I gave two talks on my first-year research project, "Ordinal Decidability via Homotopy Type Theory", at FP Lab, University of Nottingham. Here are the [abstract and slides] and a comprehensive [report].
Sep 2025: I participated in the ProofBench Lean workshop in Freiberg.
Sep 2025: I attended the Higher Structures summer school in Hamburg.
Apr 2025: I attended Midlands Graduate School in Sheffield.
Dec 2024: I attended the workshop on Categorical Logic and Higher Categories in Manchester.
- Ordinal Decidability via Homotopy Type Theory: Proofs and Results [abs]
Type Theory Cafe, Tuesday 9th December 2025, Functional Programming Lab, University of Nottingham
- Ordinal Decidability via Homotopy Type Theory: Motivations and Introduction [slide] [abs]
FP Lunch, Friday 5th December 2025, Functional Programming Lab, University of Nottingham
- Other talks.
- Languages and Computation (Spring 2026)
BSc course for second-year students at the University of Nottingham, in which we use Lean to teach Automata Theory.
- Introduction to Functional Programming (Haskell) (Spring 2026)
BSc course at the University of Nottingham.
- Introduction to Formal Reasoning (Fall 2025)
BSc course for second-year students at the University of Nottingham, in which we use Lean to teach their second course on logic.
- Mathematical Logic (Fall 2021, Spring 2022, Fall 2022)
BSc course at Sharif University of Technology, in which we taught syntax and semantics of propositional and first-order logic, their soundness and completeness, natural deduction, compactness theorem, and Löwenheim–Skolem theorems.
- Category Theory and its Applications (Fall 2022)
BSc course at Sharif University of Technology for third- and fourth-year students, in which we covered material from Emily Riehl's book and taught the basics of homological algebra.
- Foundations of Mathematics (Set Theory) (Spring 2022)
BSc course at Sharif University of Technology.
- Advanced Algebra (Fall 2022)
MSc course at Sharif University of Technology.
- Other teaching experiences
University of Nottingham, School of Computer Science,
Functional Programming Lab
Advisor: Nicolai Kraus and Tom de Jong
Dec 2024 - Now
Sharif University of Technology, Department of Mathematical Sciences
Thesis: "Mathematical object and Logical Form in Homotopy Type Theory" ( in Persian )
Advisor: Mohammad Ardeshir
Sep 2021- Feb 2024
GPA: 18.81 / 20 (first rank student)
Sharif University of Technology, Department of Mathematical Sciences \ School of Philosophy of Science
Sep 2016- Jul 2021
GPA: 17.57 / 20 (third rank student)