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, mechanized proofs, 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 15th 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 with a proof assistant; my preferred proof assistant is 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
  • Kami, a DSL for designing formally verified hardware in Coq

Past Projects

Publications & Presentations

Papers & Drafts

Proving Tree Algorithms for Succinct Data Structures
10th 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.