Mathematisches Institut | Email: | xu@math.lmu.de | |
Ludwig-Maximilians-Universität München | Office: | Block B, B420 | |
Theresienstr. 39 | Tel: | +49 (0)89 2180 4417 | |
D-80333 München | Fax: | +49 (0)89 2180 4038 |
Research interests
My research interests include constructive mathematics, (univalent/cubical/homotopy) type theory, topological methods in the theory of computation, computation extraction from proofs.
Recent events
TYPES in Munich, 7 June 2019, Munich.
Mathematical Logic and Constructivity, 20-23 August 2019, Stockholm.
CCC 2019, 2-6 September 2019, Ljubljana.
"Proof and Computation" autumn school, 20-26 September 2019, Herrsching.
Research papers
C. Xu. A Gentzen-style monadic translation of Gödel's System T. Submitted for publication, 2019.
full text (arXiv), Agda (browsable in html), slides for the MLoC'2019 talk
F. Nordvall Forsberg and C. Xu. Ordinal notations via simultaneous definitions. Submitted for publication, 2019.
full text (arXiv), Agda (browsable in html), source code, slides for the ABM'2019 talk
C. Xu. A syntactic approach to continuity of T-definable functionals. Submitted for publication, 2019.
full text (arXiv), Agda (browsable in html), source code, slides for the CCC'2018 talk
M.H. Escardó and C. Xu. The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation. T. Altenkirch (Ed.): TLCA 2015, LIPIcs 38, pp. 153-164, 2015.
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 and M.H. Escardó. A constructive model of uniform continuity, M. Hasegawa (Ed.): TLCA 2013, LNCS 7941, pp. 236-249, 2013.
Ph.D. thesis
I obtained my Ph.D. degree under the supervision of Martín Escardó at the University of Birmingham.
Thesis title: A continuous computational interpretation of type theories
abstract (pdf), full text (pdf), Agda (browsable in html), zip file
Selected Research Talks
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.
Unpublications
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)
Teaching
Lecture: Executing Proofs as Computer Programs, wintersemester 2017/18
Last modified: Tue 20th August 2019