Xuanrui (Ray) Qi
I am a master's student in computer science at
Tufts University, studying programming languages
and type theory in the TuPL research group.
I am officially advised by Professor Samuel Guyer,
and informally advised by Cyrus Omar
(University of Chicago) on my research project, in which I am extending Hazel with
features such as polymorphism and programmable edit actions. I expect to receive my M.S. degree in May 2019
and to start a PhD in computer science in the fall of 2019.
Before I started graduate school, 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 my B.S. in computer science and international
relations from Tufts University in May 2018. While I was an undergraduate, I worked with Sam Guyer on Elephant
Tracks, a GC tracing tool for Java programs.
For more details, please refer to my curriculum vitae.
My research interests are mainly in programming languages with advanced type systems,
especially dependently-typed programming languages. I am also interested in proof assistants, and in
using them to formalizing programs and mathematics. Furthermore, I like to think about applications of these
systems: dependently-typed programming with effects, language-based security, certified compilation, et cetera. Usually, I
like to write dependently-typed programs in Idris, and to hack on proofs using
I also have an interest in the mathematics of programs and types. Specifically, I am interested
in algebraic structures (and categories) in functional programming, in models and foundational
theories for types and computation, and in type-theoretic foundations of mathematics.
To a lesser extent, I am also interested in digital humanities, especially in using computational technologies to
study anthropology and popular culture related issues.
- Extending Hazel with polymorphism (à la System F) and programmable edit actions
- 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. Working draft, 2018.
Presented at various domestic venues in Japan.
[PDF] [Jacques's Slides (in Japanese)]
Elephant Tracks II: Elephant Tracks II: Practical, Extensible Memory Tracing
Xuanrui (Ray) Qi. Senior Honors Thesis, Tufts University, 2018.
[PDF] [Defense Slides]
From Tactics to Structure Editors for Proofs.
Xuanrui (Ray) Qi. Off the Beaten Track 2019 (OBT '19).
[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
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.
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". My Chinese name is written 亓璇睿 in Chinese characters, and in Mandarin
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 ㄒㄧˊ ㄏㄩㄢˊ ㄖㄨㄟˋ. In fact, even many native Chinese speakers cannot
read my name.