Xuanrui (Ray) Qi
I have just finished my M.S. in computer science at
Tufts University, and currently I am in a transitional period.
During the summer of 2019, I will be interning at SiFive, where I will work with
Murali Vijayaraghavan on formal methods
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 Chicago) and Jacques Garrigue (Nagoya University, Japan).
I am currently working on extending Hazel with
features such as polymorphism and programmable edit actions.
Before I started working on my master's degree, I visited and did research at the Graduate
School of Mathematics, Nagoya University, in Nagoya, Japan, during the summer of 2018. While I was there, I
worked with Jacques Garrigue on verifying dynamic,
succinct representations of bit vectors in Coq. Before that, I received a B.S. degree from Tufts University in May 2018.
When 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 June 15, 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.
E-mail: firstname.lastname@example.org (general use), or
email@example.com (for research-related & academic
GPG (public key): download and import, or do:
gpg --recv-keys 87F900026E06FBC8
- June 1, 2019: our paper, "Proving Tree Algorithms for Succinct Data Structures"
Reynald Affeldt, Jacques Garrigue,
and Kazunari Tanaka), was accepted to ITP 2019!
- June 3-6, 2019: I will be visiting 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.
- January 14-19, 2019: I attended POPL 2019 in Lisbon and gave a talk at the associated
workshop OBT '19. NEW: updated talk slides to talks.
My research interests are in the broad fields of programming languages and logic. More precisely, they include
type theory, functional programming, proof assistants, and the theory and practice of type-driven development, and their
intersections. I consider myself mainly a theoretical computer scientist, but I like to work on things that have
implications for practitioners as well.
My main interests at the moment including using and extending dependent type theory for programming languages and
proof assistants, and the development of programming languages for type-driven development and verification. Currently,
I am particularly interested in combining dependent types with structural polymorphism and subtyping, and in designing
interactive programming languages with typed holes, and interfaces for interacting with them, mostly from the viewpoint of
editor-as-theorem provers (see the note accompanying my OBT 2019 talk).
On the more practical side, I am interested in using proof assistants to verify programs and mathematics (see
our upcoming ITP 2019 paper on verifying algorithms for succinct data structures). On a more theoretical
side, I am interested in homotopy type theory, constructive mathematics, models for dependent type theories, and more broadly
the application of algebra, particularly category theory and algebraic topology, to theoretical computer science and logic.
- Extending Hazel with polymorphism (à la System F) and programmable edit actions
- Techniques for formal reasoning about tactic-based proofs and programming
- Refining our Coq formalization of succinct data structures
- Elephant Tracks II: extensible, efficient GC tracing
- Java heap visualization
Publications & Presentations
Papers & Drafts
Proving Tree Algorithms for Succinct Data Structures
Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, and Kazunari Tanaka. Accepted to
the 10th Conference on Interactive Theorem Proving (ITP 2019).
[PDF (local copy)] [PDF (arXiv)]
Elephant Tracks II: Practical, Extensible Memory Tracing
Xuanrui (Ray) Qi. Senior Honors Thesis, Tufts University, 2018.
[PDF] [Defense Slides]
Experience Report: Type-Driven Development of Certified Tree Algorithms in Coq
Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, and Kazunari Tanaka. Submitted to
the Coq Workshop 2019.
[Talk Abstract (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.
Exploring Corpora-Based Music Classification: Classifying Japanese Popular Music using Lyrics
Project report for COMP 150WC, "Working with Corpora", Fall 2018, Tufts University.
Securing Complex Software Systems Using Formal Verification and Specification
Course report for COMP 116, "Introduction to Computer Security", Fall 2017, Tufts University.
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 am a functional programmer. When I hack on code,
my tools of choice are OCaml, Racket, (sometimes) Haskell and Erlang. My editor of choice is
the glorious Emacs, despite that it is well known that
the standard and the best text editor.
My operating system of choice is Arch Linux, and I maintain a few
packages on the Arch User Repository.
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 prefer to just be addressed as "Ray". When I write papers, my name is
"Xuanrui (Ray) Qi". 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.