## 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, dependently-typed programming, 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 September 20, 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 &
xuanruiqi@acm.org (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

- 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!
- June 3-6, 2019: I visited Cyrus and the programming languages research group at the University of Chicago.
- 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

The main theme of my research is using types for programs and for proofs. I am interested in a broad range of issues involving types. Most of my work either involves programming in or extending functional programming languages, or hacking in a proof assistant, usually Coq.

Currently, I am mainly working on designing and implementing expressive 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.

For the latter, I am interested in the design of proof assistants based on dependent types. Particularly, I am interested in the intersection of type theory and proof engineering. I am interested in improving dependently-typed theorem provers using reflection and metaprogramming, and in extending current dependent type theories and languages to better support dependently-typed programming. I am also interested in using proof assistants, particularly Coq, to verify programs and mathematics (see our ITP 2019 paper on verifying algorithms for succinct data structures).

In mathematics, I am mainly interested in constructive algebra, geometry (in general), and (higher) category theory.

Currently, my close collaborators are Jacques Garrigue (my advisor), Cyrus Omar, and Reynald Affeldt.

#### Current Projects

- Polymorphism in Hazel
- Mechanization and verified implementation of the OCaml type system

#### Past Projects

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

#### Non-Research Technical Writing

**Formalizing the DFUDS Representation in Coq**

Project report for CS 591K, "Foundations and Pragmatics of Dependently-Typed Systems", Spring 2019,
Boston University.

(Note that the work reported is still very preliminary, and the approach outlined
might turn out not to be the most best approach.)

[PDF]

**Exploring Corpora-Based Music Classification: Classifying Japanese Popular Music using Lyrics**

Project report for COMP 150WC, "Working with Corpora", Fall 2018, Tufts University.

[PDF]

**Securing Complex Software Systems Using Formal Verification and Specification**

Course report for COMP 116, "Introduction to Computer Security", Fall 2017, Tufts University.

[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.