Xuanrui Qi
I am a graduate student at the Graduate School of Mathematics, Nagoya University, in Nagoya, Japan. I am interested in a wide range of topics in theoretical computer science and mathematics, most particularly those related to category theory, type theory, programming language theory, etc. My research advisor is Professor Jacques Garrigue, and my work is supported by the COCTI (Certifiable OCaml Type Inference) project, funded by the Tezos Foundation.
Prior to this, I worked on:
 the Kami project, towards the goal of verifying a realistic RISCV processor in Coq, with Murali Vijayaraghavan at SiFive;
 the verification of succinct data structures in Coq, with Professor Jacques Garrigue, as a research visitor here at Nagoya (in the summer of 2018);
 the Elephant Tracks project, with Professor Samuel Z. Guyer, at the Department of Computer Science, Tufts University.
I received my B.S. in computer science, double majoring in international relations and minoring in mathematics, and my M.S. in computer science, both from Tufts University, in Medford, Massachusetts, in the United States.
For more details, please refer to my curriculum vitae (last updated October 17, 2020).
I am also a formal methods consultant and freelance software engineer, most experienced in engineering formal proof and building working software systems with OCaml and Haskell, but with experience in a large variety of areas. You can check my résumé for my experience in this area.
Contact Information
Address: Graduate School of Mathematics, Nagoya University, Furocho, Chikusaku, Nagoya, Aichi, Japan 4648602
Email: me@xuanruiqi.com (general use),
xuanrui@nagoyau.jp (if you are a researcher or at an academic institution)
ORCID: 0000000220321552
Twitter: @xuanruirqi
GitHub: xuanruiqi
Keybase: xuanruiqi
Public key (PGP): download and import, or: $ gpg recvkeys 87F900026E06FBC8
Recent Activities
 March 2021: the video of our CoqPL 2021 talk is available here!
 January 2021: attended POPL 2021 online. Jacques gave our talk at the CoqPL 2021 workshop.
 November 2020: Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml has been accepted to CoqPL 2021.
 October 2020: new submission: Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml, to CoqPL 2021.
 August 2020: I attended ICFP 2020 online.
Research
Interests
Primarily, I am interested in category theory, especially categorical logic and topos theory. I am interested in the connections between category theory, type theory (such as homotopy type theory), and proof assistants such as Coq. I also enjoy using the "internal", or "synthetic" view to look at all kinds of mathematics.
More broadly speaking, I also have an interest in programming language theory and logic in computer science, as well as applications of category theory and algebraic geometry to computer science, in general. A lot of my research involve working with and coding in a proof assistant and/or dependentlytyped programming language.
Current Projects
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 typelevel 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 miniOCaml.
You can find our Coq development here, or read our brief report on this project (presented at the CoqPL Workshop 2021).
The Coq/SSReflect/MathComp algebraic structures project
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 effors are highly experimental. However, I would love to have some collaborators, and I am very open to discussions!
This is a very earlystage project, but I did give a short talk about it in November 2020. You can find the slides here.
Past Projects
 The Kami project: complete specification and verification of a practical RISCV processor using Coq
 Succinct data structures in Coq
 Elephant Tracks II: extensible, efficient GC tracing
 Java heap visualization
Publications & Presentations
Papers & Drafts
Proving Tree Algorithms for Succinct Data Structures
The 10^{th} International Conference on Interactive Theorem Proving (ITP 2019)
Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, and Kazunari Tanaka
[DOI]
[PDF]
[Local Copy]
[Slides]
[Proofs]
Elephant Tracks II: Practical, Extensible Memory Tracing
Senior Honors Thesis, Department of Computer Science, Tufts University, 2018
Xuanrui (Ray) Qi
[PDF] [Defense Slides]
[Code]
Talk Materials & Extended Abstracts
Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml
The 7^{th} 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 16^{th} Theorem Proving and Provers Meeting (TPP 2020)
Xuanrui Qi
[Slides]
Experience Report: TypeDriven Development of Certified Tree Algorithms in Coq
The Coq Workshop 2019
Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, and Kazunari Tanaka
[Extended Abstract] [For OnScreen 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)]
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;

rebuildinitramfs: 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. I do not have a Bacon number, as I have never appeared in a film as of yet.
I prefer to be referred to by the singular they, especially in a professional setting, but I am fine with he.
In an English language setting, I often prefer to just be called "Ray". Professionally, I use my full legal 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 [ㄒㄧˊ ㄏㄩㄢˊ ㄖㄨㄟˋ].
By the way, even many 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. If you are really interested about the origin of my name (and the Chinese classics), read on.
Both chracters are taken from the Book of Docuemnts (書經, or 尚書), one of the Five Classics of the Chinese classics. The first character, 璇 (of which 璿 is a variant), is taken from the following passage:
The second character, 睿, is take from: