Xuanrui Qi

Starting October 2019, I will be a graduate student at the Graduate School of Mathematics, Nagoya University. At Nagoya University, I will be working with Jacques Garrigue and others on OCaml, dependent types, theorem provers, and constructive mathematics. Currently, I am interning at SiFive, where I work with Murali Vijayaraghavan and SiFive's Formal Design and Verification Methodology Group on verifying RISC-V processors in Coq.

In May 2019, I finished my M.S. in computer science at Tufts University. At Tufts, I was officially advised by Professor Samuel Guyer and was part of the TuPL research group, but I was (and still am) mostly working remotely with Cyrus Omar (University of Michigan). With Cyrus, I am currently working on extending Hazel with features such as polymorphism and programmable edit actions.

Before that, I visited and did research at the Graduate School of Mathematics, Nagoya University, in Nagoya, Japan, during the summer of 2018, working with Jacques Garrigue on verifying dynamic, succinct representations of bit vectors in Coq. Even earlier, 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 August 20, 2019).

Note to recruiters: if you are in the industry and want to hire people to do functional programming/language design/formal methods, or any general programming languages work, you might also be interested in my résumé. I am not looking for work currently, but if you have contracting positions, please do drop me a line and I'm happy to chat.

Contact Information

Address (starting Oct 2019): Graduate School of Mathematics, Nagoya University, Furo-cho, Chikusa-ku, Nagoya, Aichi Prefecture, Japan 464-8602
E-mail: me@xuanruiqi.com (general use), or xuanruiqi@acm.org & xqi01@cs.tufts.edu (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 will be attending 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 topics involving types.

Currently, I am interested in expressive type systems for type-driven functional programming, and in making dependent types practical for verification and programming. For the former, I am interested in ML-like programming languages — particularly, I am interested in mechanized proofs about and implementation of the type systems of OCaml (working with Jacques Garrigue) and Hazel (working with Cyrus Omar).

For the latter, I am interested in the design of proof assistants based on dependent types. Particularly, I am interested in the intersection of dependently-typed programming and proof engineering. I am interested in formalizing and extending user-facing aspects of 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 upcoming ITP 2019 paper on verifying algorithms for succinct data structures).

In mathematics, I am mainly interested in constructive algebra, espcially mathematics developed using constructive type theory, and in the internal connections between topology, category theory and type theory.

Current Projects

Past Projects

Publications & Presentations

Papers & Drafts

Proving Tree Algorithms for Succinct Data Structures
Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, and Kazunari Tanaka. Accepted to the 10th International Conference on Interactive Theorem Proving (ITP 2019).
[PDF (local copy)] [PDF (arXiv)] [Slides] [Proofs]

Elephant Tracks II: Practical, Extensible Memory Tracing
Xuanrui (Ray) Qi. Senior Honors Thesis, Tufts University, 2018.
[PDF] [Defense Slides] [Code]

Talk Materials & Extended Abstracts

Experience Report: Type-Driven Development of Certified Tree Algorithms in Coq
Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, and Kazunari Tanaka. Accepted to the Coq Workshop 2019.
[Talk Abstract (PDF)] [For On-Screen Reading (PDF)]

From Tactics to Structure Editors for Proofs.
Xuanrui (Ray) Qi. Off the Beaten Track 2019 (OBT 2019).
[Talk Abstract (PDF)] [Talk Slides]

A Practical and Extensible Framework for Garbage Collection Tracing
Xuanrui (Ray) Qi. SPLASH 2018 Student Research Competition.
[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.

Before I started college in the U.S., I lived and grew up in Shenzhen, China. Now, I live in Somerville, Massachusetts. I still miss not having below-freezing temperatures in the winter.

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.