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 type systems, mathematical logic, and category theory. My research advisor is Professor Jacques Garrigue, and my work is supported by the COCTI (Certifiable OCaml Type Inference) project, which is funded by the Tezos Foundation.
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.
Prior to this, I was:
 an intern (summer 2019), then a parttime contract engineer with Murali Vijayaraghavan at SiFive, working on the Kami project, towards the goal of verifying a realistic RISCV processor in Coq;
 a research visitor here at Nagoya, with Professor Jacques Garrigue, in summer 2018, working on the verification of succinct data structures in Coq;
 a research assistant on the Elephant Tracks project, under Professor Samuel Z. Guyer at the Department of Computer Science, Tufts University;
 a student at Tufts University, from which I received a M.S. in Computer Science and a B.S. As an undergraduate, I majored in computer science and international relations, and minored in mathematics.
For more details, please refer to my curriculum vitae (last updated October 17, 2020).
I am welcome to offers for consulting and contracting work! My main field of expertise is in formal methods, software correctness, and highassurance software (especially proof engineering in the Coq theorem prover), but I am also experienced in engineering and developing programming language infrastructure and runtime, as well as in general software development in OCaml and Haskell. Please consult me for your verification needs! If you are interested, you may want to look at my résumé, and shoot me an email at me@xuanruiqi.com!
Contact Information
Address: Graduate School of Mathematics, Nagoya University, Furocho, Chikusaku, Nagoya, Aichi, Japan 4648602
Email: me@xuanruiqi.com (general use),
xuanrui@nagoyau.jp (for researchrelated & academic
communication)
ORCID: 0000000220321552
Twitter: @xuanruirqi
GitHub: xuanruiqi
Keybase: xuanruiqi
GPG (public key): download and import, or do: gpg recvkeys 87F900026E06FBC8
Recent Activities
 October 2020: Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml has been accepted to CoqPL 2021, and Jacques gave the talk online.
 October 2020: new submission: Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml, to CoqPL 2021.
 August 2020:I attended ICFP 2020 online.
 JuneJuly 2020: I attended PLDI 2020, IJCAR/FSCD 2020 & and LICS/ICALP 2020 virtually.
 Nov 1819, 2019: I attended the 15^{th} TPP meeting at the National Institute of Informatics in Tokyo.
Research
Main Interests
I have a variety of research interests, both in theoretical computer science and (pure) mathematics. Often, my interests involve a structural and constructive pointofview, and are inspired by ideas in mathematical logic and type theory. Machinecheckable proofs in a proof assistant, such as Coq, play an important role.
Computer science
 Generalized algebraic data types (GADTs) and their type inference
 Bidirectional type checking and constraintbased type inference algorithms for MLlike languages
 Formalizing mathematics in the Coq proof assistant
 Type theory for mathematical reasoning, and homotopy type theory
Mathematics
I am especially interested in "abstract", or perhaps "Grothendieckstyle" mathematics. I like to study and use categorical structures in the context of other fields of mathematics, most particularly algebraic geometry. Broadly speaking, the areas/lines of research I am most interested in are:
 Topos theory and categorical logic
 Synthetic ("internal logic") approach to mathematics, particularly algebraic geometry
 Modern algebraic geometry in general, especially parts that use heavily categorical techniques
Current Projects
 COCTI (Certifiable OCaml Type Inference), more specifically:
 Certified ML implementation with structural polymorphism and GADTs
 Specification for and soundness of GADTs in OCaml
 The Coq/SSReflect/MathComp algebraic geometry 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. Currently, I am focused on the tools required to define a scheme, the main subject of study in (Grothendieck's) algebraic geometry. 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!
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
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, 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} Workshop on Coq for Programming Languages (CoqPL 2021)
Xuanrui Qi, Jacques Garrigue
[Extended Abstract]
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.
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 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.

initramfs rebuild script for Arch Linux: a script that mimics
the behavior of
mkinitcpio P
for Dracut users.  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, 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 line:
在璿璣玉衡，以齊七政。肆類于上帝，禋于六宗，望于山川，徧于群神。輯五瑞。既月乃日，覲四岳群牧，班瑞于群后。
He examined the pearladorned turning sphere, with its transverse tube of jade, and reduced to a harmonious system (the movements of) the Seven Directors. Thereafter, he sacrificed specially, but with the ordinary forms, to God; sacrificed with reverent purity to the Six Honoured Ones; offered their appropriate sacrifices to the hills and rivers; and extended his worship to the host of spirits. He called in (all) the five jadesymbols of rank; and when the month was over, he gave daily audience to (the President of) the Four Mountains, and all the Pastors, (finally) returning their symbols to the various princes.
The second character, 睿, is take from:
貌曰恭，言曰從，視曰明，聽曰聰，思曰睿。恭作肅，從作乂，明作哲，聰作謀，睿作聖。
(The virtue of) the bodily appearance is respectfulness; of speech, accordance (with reason); of seeing, clearness; of hearing distinctness; of thinking, perspicaciousness. The respectfulness becomes manifest in gravity; accordance (with reason), in orderliness; the clearness, in wisdom; the distinctness, in deliberation; and the perspicaciousness, in sageness.