Profile
I'm a postdoctoral research fellow working with Sam Sanders at the Munich Center for Mathematical Philosophy (MCMP).
Before coming to the MCMP, I completed my Ph.D. degree under the supervision of Martín Escardó in the School of Computer Science at the University of Birmingham.
Research interests
My research interests include constructive mathematics, (homotopy) type theory, topological methods in the theory of computation, computation extraction from proofs.
Ph.D. thesis
My Ph.D. thesis is entitled 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. Accepted for publication in Annals of Pure and Applied Logic, 2015.
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
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
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 5th Jan 2017