## Xuanrui Qi

I am a graduate student at the Graduate School of Mathematics, Nagoya University (名古屋大学大学院多元数理科学研究科). My research advisor is Jacques Garrigue, and I mainly work on typed functional programming languages, computer-assisted interactive proof, type theory, and category theory.

Before this, I interned at SiFive during the summer of 2019, working with Murali Vijayaraghavan on verifying RISC-V processors in Coq. In May 2019, I finished my M.S. in computer science at Tufts University, where I was officially advised by Professor Samuel Guyer and affiliated with the TuPL research group. During the summer of 2018, I was a research visitor here at Nagoya University working with Jacques, and before that, I received a B.S. degree from Tufts University in May 2018. While I was an undergraduate, I majored in computer science and international relations, minored in mathematics, and worked with Professor Sam Guyer on redesigning Elephant Tracks, a GC tracing tool for Java programs.

For more details, please refer to my curriculum vitae (last updated November 27, 2019).

### 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 (for research-related & academic
communication)

**ORCID: ** 0000-0002-2032-1552

**Twitter:** @xuanruirqi

**GitHub:** xuanruiqi

**Keybase:** xuanruiqi

**GPG (public key):** download and import, or do: `gpg --recv-keys 87F900026E06FBC8`

### Recent Activities

- Nov 18-19, 2019: I attended the 15
^{th}TPP meeting at the National Institute of Informatics in Tokyo. - Sept 8-12, 2019: I attended ITP 2019 and the Coq Workshop 2019 in Portland, Oregon.
- July 2, 2019: our talk proposal on type-driven development of correct tree algorithms in Coq has been accepted to the Coq Workshop 2019!
- June 1, 2019: our paper, "Proving Tree Algorithms for Succinct Data Structures" (coauthored with Reynald Affeldt, Jacques Garrigue, and Kazunari Tanaka), has been accepted to ITP 2019!
- May 2019: I have graduated from Tufts University (again), this time with a M.S. in computer science. All my previous Tufts email addresses will still work.

### Research

#### Interests

I like theoretical computer science and mathematics, and especially their intersection. For the former, I am mostly interested in programming language theory and type theory; for the latter, I am interested in category theory, topology, and mathematical logic. A lot of my work involves writing proofs and (sometimes) implementing type systems; I believe that the right way to approach this is to work in a proof assistant. Much of my work is conducted in my preferred proof assistant, Coq.

Now, I am mainly working on designing, implementing and formalizing type systems for functional programming languages, and on dependently-typed programming. Particularly, I am interested in the ML family programming languages — particularly, I am interested in the implementation of and mechanized proofs about the type systems of OCaml and Hazel. Lately, I am studying type inference for and the semantics of generalized algebraic data types (GADTs).

Towards more pure mathematics, I am interested in type theory and category theory, especially their intersections. Specifically, I lean towards approaching type theory and logic from a categorical and/or topological point of view, and vice versa. Currently, this mostly means homotopy type theory and topos theory — although I know little about either, and I am mainly learning about things. I am also interested in constructive mathematics and formal topology in general.

#### Current Projects

- Specification and type inference for GADTs in OCaml
- Polymorphism in Hazel
- Complete verification of a practical RISC-V processor in Kami, a DSL for designing formally verified hardware in Coq

#### Past Projects

- 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

**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)]

### Software

Over the course of many years, I created some software, mainly for personal use, but maybe also of public interest:

- 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.
- Brainf**k: a Brainf**k interpreter written in C++11, for fun and (probably not) profit. This was written years ago when I was a sophomore.

Of course, I create some more serious 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 addressed as "Ray". My Chinese name (Xuanrui Qi) is written 亓璇睿 in Chinese characters, and in Mandarin it is pronounced /tɕʰi˧˥ ɕɥɛn˧˥ ɻwei̯˥˩/ (in 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 read the Chinese characters in my name.