I am a researcher working in formal methods and mathematical logic.
Previously, I was a static analysis scientist at SonarSource in Bochum. Before that, I was a researcher in the Safety and Security group at fortiss in Munich during 2020-2022, and a Humboldt postdoctoral research fellow at LMU Munich during 2017-2020. I obtained my Ph.D. degree at the University of Birmingham in 2015 under the supervision of Prof. Martín Hötzel Escardó.
My research interests include static analysis, formal verification, type theory, constructive mathematics, program extraction from proofs, and other topics in mathematical logic, as well as origami and its mathematics.
T. de Jong, N. Kraus, F. Nordvall Forsberg and C. Xu. Ordinal exponentiation in homotopy type theory. LICS 2025, Distinguished Paper.
U. Schöpp, F. Faghih, S. Bandopadhyay, H. Joumaa, A. Ibrahim, C. Xu, X. Ye, and T. Dimitrakos. Static and dynamic analysis of a usage control system. SACMAT 2024.
T. de Jong, N. Kraus, F. Nordvall Forsberg and C. Xu. Set-theoretic and type-theoretic ordinals coincide. LICS 2023.
N. Kraus, F. Nordvall Forsberg and C. Xu. Type-theoretic approaches to ordinals. Theoretical Computer Science vol. 957, 2023.
U. Schöpp, C. Xu, A. Ibrahim, F. Faghih, and T. Dimitrakos. Specifying a usage control system. SACMAT 2023.
U. Schöpp and C. Xu. Inferring region types via an abstract notion of environment transformation. APLAS 2022.
LNCS, arXiv, source code, slides (APLAS'22)
S. Erbatur, U. Schöpp and C. Xu. Type-based enforcement of infinitary trace properties for Java. PPDP 2021.
ACM, arXiv, source code, slides (PPDP'21)
N. Kraus, F. Nordvall Forsberg and C. Xu. Connecting constructive notions of ordinals in homotopy type theory. MFCS 2021.
LIPIcs, arXiv, Agda-html, source code, slides (BIRS-Hangzhou)
U. Schöpp and C. Xu. A generic type system for featherweight Java. FTfJP 2021.
C. Xu. A Gentzen-style monadic translation of Gödel's System T. FSCD 2020.
LIPIcs, arXiv, Agda-html, source code, slides (MLoC'19)
F. Nordvall Forsberg, C. Xu and N. Ghani. Three equivalent ordinal notation systems in cubical Agda. CPP 2020.
ACM, arXiv, Agda-html, source code, slides (ABM'19)
C. Xu. A syntactic approach to continuity of T-definable functionals. Logical Methods in Computer Science 16(1), 2020.
LMCS, arXiv, Agda-html, source code, slides (CCC'18)
P. Oliva and C. Xu. On the Herbrand functional interpretation. Mathematical Logic Quarterly 66(1), 2020.
M.H. Escardó and C. Xu. A constructive manifestation of the Kleene-Kreisel continuous functionals. Annals of Pure and Applied Logic 167(9), 2016.
C. Xu. A continuous computational interpretation of type theories. PhD thesis, University of Birmingham, 2015.
M.H. Escardó and C. Xu. The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation. TLCA 2015.
C. Xu and M.H. Escardó. A constructive model of uniform continuity. TLCA 2013.
From double-negation translation of proofs to static analysis of code (slides). Type Theory, Constructive Mathematics and Geometric Logic, CIRM, Marseille, May 2023.
Various approaches to computing moduli of continuity (slides). Lecture at the Proof and Computation autumn school, Fischbachau, September 2022.
A certified library of ordinal arithmetic (slides, Agda-html). Continuity, Computability, Constructivity (CCC), Birmingham/online, September 2021.
Connecting constructive notions of ordinals in Homotopy Type Theory (slides). New Frontiers in Proofs and Computation, Hangzhou/online, September 2021.
Various structures of T-definable functionals via a Gentzen-style translation (slides). Mathematical Logic and Constructivity, Stockholm, August 2019.
Ordinal notations via simultaneous definitions (slides). ABM Spring 2019, Munich, May 2019.
A syntactic approach to continuity of Gödel's system T definable functionals (slides). Continuity, Computability, Constructivity (CCC), Faro, September 2018.
Unifying functional interpretations of nonstandard/uniform arithmetic (slides). Logic Colloquium, Udine, July 2018.
A univalent approach to constructive mathematics (slides). Mathematical Logic and its Applications, Kanazawa, March 2018.
Using function extensionality in Agda, (non-)computationally (slides). Oberseminar Mathematische Logik, LMU Munich, December 2017.
A syntactic treatment of majorizability of T-definable functionals (Agda code in html)
An Agda implementation of Oliva & Steila's A direct proof of Schwichtenberg's bar recursion closure theorem (code in html)
Implementing the nonstandard Dialectica interpretation (notes in pdf, slides, Agda code in html)
Universes in sheaf models (notes in pdf)
The Dialectica interpretation in Agda (code in html)
Course: Executing Proofs as Computer Programs, winter semester 2021/22, Mathematics Institute, LMU Munich
Course: Executing Proofs as Computer Programs, winter semester 2017/18, Mathematics Institute, LMU Munich
Last modified: Tue 7 Apr 2026