fortiss GmbH | Email: | lastname@fortiss.org | |
Guerickestraße 25 | or | lastname@math.lmu.de | |
80805 München |
I'm a researcher in the Safety and Security group at fortiss. Before joining fortiss, I was a Humboldt postdoctoral research fellow at LMU Munich. I obtained my Ph.D. degree under the supervision of Martín Escardó at the University of Birmingham.
My research interests include type theory and its applications (especially in program analysis and verification), constructive mathematics, program extraction from proofs, many other things.
S. Erbatur and U. Schöpp and C. Xu. Type-based enforcement of infinitary trace properties for Java. PPDP 2021.
arXiv, source code, slides (PPDP'21)
N. Kraus and 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.
F. Nordvall Forsberg and 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. LMCS 16(1), pp. 22:1-22:11, 2020.
LMCS, arXiv, Agda-html, source code, slides (CCC'18)
P. Oliva and C. Xu. On the Herbrand functional interpretation. MLQ 66(1), pp. 91-98, 2020.
M.H. Escardó and C. Xu. A constructive manifestation of the Kleene-Kreisel continuous functionals. Ann. Pure Appl. Logic, 167(9), pp. 770-793, 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.
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, wintersemester 2017/18
Last modified: Wed 22 September 2021