---

I am a PhD student in Mathematics at the University of Western Ontario under the supervision of Chris Kapulkin

My research centers around applying methods of abstract homotopy theory to study semantics of dependent type theories

Currently I am on a leave of absence working as a functional compiler engineer at Heliax

Contact me: agureev (at) uwo (dot) ca

---

• Summer 2022:
  HoTTEST Summer School

---

• September 2021 - present:
  PhD, Mathematics, University of Western Ontario
• September 2020 - August 2021:
  MSc, Mathematics, University of Western Ontario
• September 2016 - May 2020:
  BA, Mathematics and Philosophy, Boston University

---

A couple of years ago I created short tutorials to help people start using Coq and Agda interactive theorem provers:

• Coq Tutorial
• Agda Tutorial