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, (homotopy) type theory, topological methods in the theory of computation, computation extraction from proofs.
Teaching
Lecture: Executing Proofs as Computer Programs, wintersemester 2017/18
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
Research papers
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.
Selected Research Talks
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.
Unifying (Herbrand) functional interpretations of (Nonstandard) arithmetic (slides). Proof and Computation, Verona, October 2017.
Unpublications
A syntactic approach to continuity of Gödel's system T definable functionals (slides, Agda code in html)
An inductive-recursive approach to ordinals (notes in pdf, Agda code in html)
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)
Last modified: Mon 1st October 2018