Published Papers

1. Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka. Proving Tree Algorithms for Succinct Data Structures. 10th International Conference on Interactive Theorem Proving (ITP 2019).
   [Paper] [Local Copy]

Theses

Master's thesis: Type Theory and the Logic of Toposes. Graduate School of Mathematics, Nagoya University, 2021.
[Thesis]

Workshop Papers & Extended Abstracts

1. Jacques Garrigue, Xuanrui Qi. Formalizing OCaml GADT Typing in Coq. ML Family Workshop 2021.
   [Paper] [Slides]
2. Xuanrui Qi, Jacques Garrigue. Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml. 7th International Workshop on Coq for Programming Languages (CoqPL 2021).
   [Paper] [Slides]
3. Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari Tanaka. Experience Report: Type-Driven Development of Certified Tree Algorithms in Coq. Coq Workshop 2019.
   [Paper] [Long Version] [Slides]
4. Xuanrui Qi. From Tactics to Structure Editors for Proofs. Off the Beaten Track 2019.
   [Extended Abstract] [Slides]
5. Xuanrui Qi. A Practical and Extensible Framework for Garbage Collection Tracing. SPLASH 2018 Student Research Competition.
   [Extended Abstract]

Talk Materials

1. Towards Synthetic Riemann-Roch. 4th Workshop on Synthetic Algebraic Geometry (SAG4), Gothenberg, Sweden. March 2024.
   [Slides]
2. Synthetic geometry in Lean 4: early experiments with Mathlib4. The 19th Theorem Proving and Provers Meeting (TPP 2023), Tokyo, Japan. October 2023.
   [Slides]
3. On operator algebras, linear logic and categorical quantum mechanics. Algebra, Logic and Geometry in Informatics 2023 (ALGI 34) / 第34回代数、論理、幾何と情報科学研究集会, Fujisawa, Japan. September 2023.
   [Slides]
4. Rings, categories and schemes in Coq II: the functor of points. The 17th Theorem Proving and Provers Meeting (TPP 2021), Kitami, Japan. November 2021.
   [Slides]
5. Rings, categories and schemes in Coq/SSReflect. The 16th Theorem Proving and Provers Meeting (TPP 2020), online. November 2020.
   [Slides]