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, but currently I am (informally) working with Cyrus Omar (University of Chicago). I am currently working on 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 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 April 3, 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 in the near future, but if you're interested, please do drop a line and I'm happy to discuss potential opportunities in the future.

Contact Information

Physical Address: 161 College Avenue, Department of Computer Science, Halligan Hall, Medford, MA 02155, USA [Google Maps]
E-mail: me@xuanruiqi.com or xqi01@cs.tufts.edu (for research-related & academic communication)
ORCID: 0000-0002-2032-1552
Twitter: @xuanruirqi
GitHub: xuanruiqi
Public Key (GPG): download

Recent Activities

  • January 14-19, 2019: attended POPL 2019 in Lisbon. Gave a talk at the associated workshop OBT '19. NEW: updated talk slides to talks.
  • November 7-9, 2018: attended SPLASH/OOPSLA 2018 in Boston. Presented my poster at the SRC.
  • September 24-29, 2018: attended ICFP 2018 in St. Louis, USA.
  • June-August 2018: visited and worked with Jacques Garrigue in Nagoya, Japan.

Research

Interests

Broadly speaking, my research interests are in the broad field programming languages and formal methods. 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 Coq. Recently, I have also been using Agda increasingly.

In addition to the theory, I am interested in applying methods from programming languages to computer systems and security, especially in combining systems programming with types and verification. I am interested in compilers, system-level semantics (and mechanizing them), verifying system-level programs, langauge-based security, programming abstractions and type systems for concurrent and distributed computing, and the interaction between types and memory management.

Finally, I also have an interest in the mathematics of programs and types and in constructive foundations of mathematics. Specifically, I am interested in algebraic structures (and categories) in functional programming, models and foundational theories for types and computation, type-theoretic foundations of mathematics, and the connections between type theory, topology and constructive mathematics.

My secondary, and less formal research interests are in the digital humanities and computational media: applied computational linguistics, computational musicology & music theory, and interactive computing interfaces (especially developing interactive programming languages).

Keywords I usually look for: dependent types, proof assistant, type-driven development.

Current Projects

  • 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

Past Projects

  • 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 (Ray) Qi, and Kazunari Tanaka. Submitted to the 10th Conference on Interactive Theorem Proving (ITP 2019).
[PDF (local copy)] [PDF (arXiv)] [Jacques's Slides (in Japanese)] [Proofs]

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

Talk Materials

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

Securing Complex Software Systems Using Formal Verification and Specification
Course report for COMP 116, "Introduction to Computer Security", Fall 2017, Tufts University.
[PDF]

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 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 ed is 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". 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.