I am a mathematics PhD student at the University of Western Ontario,
supervised by Dan Christensen. I
like (homotopy) type theory, (higher) category theory, and mathematical
logic of all kinds.
I also like formalising mathematics in proof assistants, currently focused on doing
constructive mathematics in
Coq/Rocq (in particular, the
Coq-HoTT library), and also having worked with
Rzk and
Lean.
I finished my master's at the University of Bonn in August 2024. I wrote
my thesis on simplicial type
theory, supervised by
Nima Rasekh and
Floris van Doorn.
Before that, I got my Bachelor's degree from the Aristotle University of
Thessaloniki.
I look like this.
Contact Information
I'm guessing that this website is currently an accessibility nightmare. I appreciate any criticism or suggestions on how to improve it.
News
Old News
-
[09-12.2025] I am supervising an undergraduate
student learning about axiomatic set theory, as part of the directed
reading program at Western.
-
[09-12.2025] Together with Thomas
Thorbjørnsen, we are organising a
reading seminar on topos theory.
-
[02-04.2025] I supervised an undergraduate
student learning about model theory, as part of the directed
reading program at Western.
-
[11.2024-05.2025] I am formalising various
forms of the bar induction axiom and their implications in Coq
(in particular, the Coq-HoTT library). I'm also thinking about the
consequences of assuming such axioms from constructive mathematics in
homotopy type theory.
-
[07-08.2024] Together with Nima Rasekh, we
are wondering what we can prove about 2-Segal spaces synthetically, in
the setting of simplicial type theory.