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.
N. Kraus and F. Nordvall Forsberg and C. Xu. Connecting constructive notions of ordinals in homotopy type theory
S. Erbatur and U. Schöpp and C. Xu. Type-based enforcement of infinitary trace properties for Java
C. Xu. A Gentzen-style monadic translation of Gödel's System T. FSCD 2020.
LIPIcs, arXiv, Agda (browsable in html), source code, slides for the MLoC'2019 talk
F. Nordvall Forsberg and C. Xu and N. Ghani. Three equivalent ordinal notation systems in cubical Agda. CPP 2020.
ACM, arXiv, Agda (browsable in html), source code, slides for the ABM'2019 talk
C. Xu. A syntactic approach to continuity of T-definable functionals. LMCS 16(1), pp. 22:1-22:11, 2020.
LMCS, arXiv, Agda (browsable in html), source code, slides for the CCC'2018 talk
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.
abstract (pdf), full text (pdf), Agda (browsable in html), zip file
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.
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: Thur 8 April 2021