Xuanrui Qi

I am a second-year Ph.D. student at the Graduate School of Mathematics, Nagoya University, in Nagoya, Japan. My research advisor is Professor Jacques Garrigue. I am a research fellow in the THERS Interdisciplinary Frontier Next Generation Researcher Program, and a participant in the COCTI (Certifiable OCaml Type Inference) project. My research is financially supported by the Japan Science and Technology Agency (JST) and the Tezos Foundation.

Broadly speaking, my research is in category theory and applied algebraic topology. Currently, I am interested in two research topics: (1) category theoretic foundations of geometry, particularly via differential and tangent categories, and (2) applied category theory from quantum programs and machine learning. I am also interested in a wide range of other topics in mathematics and computer science, especially those involving computer formalization with the Coq proof assistant.

I received an M.S. in mathematics in 2021, also from the Graduate School of Mathematics, Nagoya University. I wrote my thesis on the connection between toposes and the semantics of type theory. Before that, I received a B.S. in computer science, with a double major in international relations and minor in mathematics, and an M.S. in computer science, both from Tufts University, in the United States.

For more details, please refer to my curriculum vitae (last updated September 28, 2021).

Contact Information

Address: Graduate School of Mathematics, Nagoya University, Furo-cho, Chikusa-ku, Nagoya, Aichi, Japan 464-8602
E-mail: me@xuanruiqi.com (general use), xuanrui@nagoya-u.jp (if you are a researcher or at an academic institution)
ORCID: 0000-0002-2032-1552
Twitter: @xuanruirqi
GitHub: xuanruiqi
Public key (PGP): available from a keyserver: $ gpg --recv-keys 87F900026E06FBC8. If that is not possible, you can also download and import the key.

Recent Activities

  • August-December 2022: I have attended/will be at a few domestic workshops and conferences in Japan.
  • July 2022: I attended ACT 2022 online.
  • August 2021: attended ICFP 2021 online. Jacques gave our talk at the ML Family workshop.
  • July 2021: successfully defended my master's thesis, which is a survey of topos-theoretic models of type theory.
  • June 2021: new talk (co-authored with Jacques Garrigue), "Formalizing OCaml GADT Typing in Coq", accepted to the ML Family Workshop 2021.
  • March 2021: the video of our CoqPL 2021 talk is available here!

Research

Interests

  • categorical foundations of geometry, differential and tangent categories
  • differential computation applications of synthetic differential geometry
  • categorical formalism for quantum programs and machine learning
  • ∞-category theory and more general "categorified"/"derived" mathematics
  • computer-assisted theorem proving and formalized mathematics
  • more generally, category theory, type theory, and logic in computer science

Current Research

Explaining the geometry of machine learning via persistence and sheaf theory

The goal of my research is to elucidate the geometric structure of machine learning algorithms via category theory, and especially via sheaf theory. Towards this goal, I study persistent (co)homology and topological data analysis. Particularly, I am interested in topological persistence in sheaf-theoretic settings, and in using a combination of TDA and sheaf-theoretic methods to explain the structure of neural networks.

Applied synthetic differential geometry and the mathematics of differentiable computation

I am also interested in how synthetic differential geometry (SDG) can be used for differentiable computation and related areas. For example, it is known that SDG can explain automatic differentiation for higher-order functions nicely. I am interested in further generalizations, as well as potential connections to machine learning theory (e.g., the connection between ML and PDEs/dynamical systems).

The aforementioned research projects are supported by a fellowship from the THERS Interdisciplinary Frontier Next Generation Researcher Program, funded by the Japan Science and Technology Agency (JST) SPRING Program, grant number JPMJSP2125.

Categorical foundations of geometry

I am interested in developing the ideas of modern geometry (such as vector bundles, tangent bundles, cohomology, abstract homotopy theory, etc.), using a purely categorical formulation. Currently, I am mostly interested in connections between the language of tangent categories and algebraic/differential geometry.

COCTI (Certifiable OCaml Type Inference)

I am mainly working (with Jacques Garrigue) on designing an expressive core language for OCaml, with formalized semantics and typing rules, that supports structural polymorphism and type-level equality witnesses. This core language is expressive enough to encode most of modern OCaml (except for the imperative part and the module language) without much hassle. We aim to develop a mechanized specification and semantics for this core language, and prove the soundness of and principality of type inference for this mini-OCaml.

You can find our Coq development here, or read our brief report on this project (presented at the CoqPL Workshop 2021).

Formalization of mathematics in Coq

Starting from what is already done in the Coq Mathematical Components library, I build the necessary building blocks required to develop modern algebraic geometry, commutative algebra, and homological algebra. Currently, I am focused on developing basic categorical notions, as well as some basic theorems in commutative algebra. This project is still in a nascent stage, and current development efforts are highly experimental. However, I would love to have some collaborators, and I am very open to discussions!

This is a very early-stage project, but I did give short talks about it in November 2020 and 2021. You can find the slides here and here.

Past Projects

Publications & Presentations

Papers & Drafts

Proving Tree Algorithms for Succinct Data Structures
The 10th International Conference on Interactive Theorem Proving (ITP 2019)
Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, and Kazunari Tanaka
[DOI] [PDF] [Local Copy] [Slides] [Proofs]

Talk Materials & Extended Abstracts

Rings, Categories and Schemes in Coq (II): Formalizing the Functor of Points in Coq
The 17th Theorem Proving and Provers Meeting (TPP 2021)
Xuanrui Qi
[Slides]

Formalizing OCaml GADT Typing in Coq
The ML Family Workshop 2021 (ML 2021)
Jacques Garrigue, Xuanrui Qi
[Extended Abstract] [Slides]

Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml
The 7th International Workshop on Coq for Programming Languages (CoqPL 2021)
Xuanrui Qi, Jacques Garrigue
[Extended Abstract] [Slides] [Talk Video on YouTube]

Rings, Categories and Schemes in Coq
The 16th Theorem Proving and Provers Meeting (TPP 2020)
Xuanrui Qi
[Slides]

Experience Report: Type-Driven Development of Certified Tree Algorithms in Coq
The Coq Workshop 2019
Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, and Kazunari Tanaka
[Extended Abstract] [For On-Screen Reading] [Slides]

From Tactics to Structure Editors for Proofs
Off the Beaten Track 2019 (OBT 2019)
Xuanrui (Ray) Qi
[Extended Abstract] [Slides]

A Practical and Extensible Framework for Garbage Collection Tracing
SPLASH 2018 Student Research Competition
Xuanrui (Ray) Qi
[Extended Abstract (PDF)]

Theses

Type Theory and the Logic of Toposes
Master's Tzhesis, Graduate School of Mathematics, Nagoya University, 2021
Xuanrui Qi
[PDF] [Defense Slides]

Elephant Tracks II: Practical, Extensible Memory Tracing
Senior Honors Thesis, Department of Computer Science, Tufts University, 2018
Xuanrui (Ray) Qi
[PDF] [Defense Slides] [Code]

Software

I maintain the following projects that are probably of public interest:

  • the alpm Gem, currently under development. This is a Ruby binding to libalpm, the Arch Linux package management library;
  • rebuild-initramfs: a script that mimics mkinitcpio presets for Dracut users on Arch Linux. It is available on the AUR.

Over the course of many years, I created a lot of software for personal use. However, in the rare case that other people are interested, they are also publicly available:

  • grading tool (currently unnamed): a set of Ruby scripts to help automate the task of remote grading & grade management. Put grades in YAML files, and get grade summaries & grading emails sent out automatically.
  • DynRuby: a JavaScript tool to display ruby annotations on hover. You can find a demo here.
  • RubyPP: ruby annotation preprocessor for Markdown. Converts ruby annotated Markdown to GitHub flavored markdown.

Of course, I create some more interesting software for my research. These can be found in the corresponding section.

I am a functional programmer. My programming language of choice is OCaml, but I sometimes also code in Haskell, and to a lesser extent in Idris and Erlang. In the rare occasion that I code imperatively, I usually use Ruby or sometimes Python. My editor of choice is the glorious Emacs, despite that it is well known that ed is the standard and the best text editor. My operating system of choice is Arch Linux: please see my Linux page for my engagements in the Linux community.

Personal

My Erdős number is at most 5, via the shortest known collaboration path: Reynald Affeldt, Naoki Kobayashi, Magnús M. Halldórsson, Márió Szegedy, Paul Erdős.

In an English language and casual setting, I often prefer to just be called "Ray". Professionally, I always use my full name. My name is written 亓璇睿 in Chinese characters (hanzi/kanji), and in Mandarin (technically, "modern standard Mandarin") it is pronounced /tɕʰi˧˥ ɕɥɛn˧˥ ɻwei̯˥˩/ (IPA) . I find the best approximation (modulo tones) to be the Japanese katakana: チー・シュエンルイ. If you can read Hanyu Pinyin or Bopomofo (Zhuyin Fuhao), it is pronounced [qí xuán ruì] or [ㄒㄧˊ ㄏㄩㄢˊ ㄖㄨㄟˋ]. I sometimes prefer to be referred to by the singular they, especially in writing, but most of the time I go with he.

Even my any native Chinese speakers cannot pronounce the Chinese characters in my name, as my surname is an extremely rare one (by Chinese standards). There are about 130,000 people with my surname in mainland China and a few hundred more in Taiwan; all of us hail from Laiwu (莱芜), a small city near Ji'nan, the capital of Shandong Province.