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 computational continuous 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
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
Universes in sheaf models (pdf)
The Dialectica interpretation in Agda (code in html)
Last modified: Sun 15th May 2016