Xuanrui Qi

NEWS (March 2025)💼: I'm due to graduate in late 2025, and I am currently looking for a job with prospective start date of October 2025! I am open to all kinds of work in software. My expertise is in programming language design & implementation, formal methods, runtime systems and blockchain, but I am also willing to take up other jobs requiring a strong mathematical background such as optimization and data science. For details, please refer to this page.
仕事を探しています．詳しくはこのページを読んでくださると幸いです．

I am Xuanrui Qi (亓璇睿), a fourth-year PhD student at the Graduate School of Mathematics, Nagoya University advised by Professors Jacques Garrigue and Lars Hesselholt. Broadly speaking, my research interests are in type theory and topos theory, and particularly their application to geometry and topology.

I hold two master's degrees: an MS in mathematics from Nagoya University (2021), and an MS in computer science from Tufts University in the United States (2019). I did my undegraduate studies at, and received my bachelor's degree in computer science and international relations from Tufts University in 2018.

I am fortunate to be supported financially by the Japan Science and Technology Agency (JST)'s SPRING program, through participation in the Tokai National Higher Education & Research System (THERS) "Make New Standards Program for Next Generation Researchers".

You can find a copy of my CV here.

Contact Information

Research

My research interests could be broadly categorized as topos-theoretic type theory (i.e., using type theory as a language to describe topoi). Currently, I am mostly interested in homotopy type theory (HoTT) and ∞-topos theory, and in particular the use of modal HoTT as a language for developing geometry and topology, most importantly algebraic geometry, internally to an ∞-topos.

My doctoral thesis will be on a synthetic theory of étale sheaves and étale cohomology formalized in modal HoTT.

I view my work as a natural extension of the line of work pioneered by Alexander Grothendieck in the 1970s and 80s, and an internalization of Grothendieck's relative point of view. By viewing topoi as abstracted categories of sheaves, and geometric objects as structured sheaves, type theory naturally becomes a language for conveying geometric information, and an essentially functorial (i.e. Grothendieckian) view of geometry is obtained without extra effort.

I am also interested in various areas related to category theory and/or type theory:

  • abstract approaches to non-commutative geometry;
  • categorical foundations of quantum information;
  • categorical logic in general;
  • the design and implementation of proof assistants;
  • formalized mathematics;
  • applied algebraic topology and in particular persistence theory.

Previously I also did research in various areas in theoretical computer science, such as design and implementation of type systems. I was involved in the formalization of OCaml's type system.

Trivia

I have an Erdős number of at most 5.