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.
Research Talks
Unifying (Herbrand) functional interpretations of (Nonstandard) arithmetic (slides). Proof and Computation, Verona, October 2017.
Extracting Computer Programs from Nonstandard Proofs (slides). Logic and its Applications, Mathematics Institute LMU, October 2016.
Sheaf models of type theory in type theory (slides). Mathematics for Computation (M4C), Niederalteich, Germany, May 2016.
A constructive manifestation of the Kleene-Kreisel continuous functionals (slides). Arbeitstagung Bern-München (ABM), Mathematics Institute LMU, December 2015.
When is the Kleene–Kreisel hierarchy full? (slides). Math Lunch talk in School of Computer Science, the University of Birmingham, November 2013.
A constructive model of unform continuity (slides). Typed Lambda Calculi and Applications (TLCA'2013), Eindhoven, the Netherlands, June 2013.
A constructive model of unform continuity (slides). Fourth Workshop on Formal Topology (4WFTop), Ljubljana, June 2012.
Unpublications
A syntactic approach to continuity of Gödel's system 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 (pdf, slides, Agda code in html)
Universes in sheaf models (pdf)
The Dialectica interpretation in Agda (code in html)
Last modified: Wed 20th June 2018