The inconsistency of a Brouwerian continuity principle with the Curry–Howard interpretation M Hötzel Escardó, C Xu 13th International Conference on Typed Lambda Calculi and Applications (TLCA …, 2015 | 45 | 2015 |

A constructive model of uniform continuity C Xu, M Escardó Typed Lambda Calculi and Applications: 11th International Conference, TLCA …, 2013 | 22 | 2013 |

A constructive manifestation of the Kleene–Kreisel continuous functionals M Escardó, C Xu Annals of Pure and Applied Logic 167 (9), 770-793, 2016 | 21 | 2016 |

A continuous computational interpretation of type theories C Xu University of Birmingham, 2015 | 13 | 2015 |

Three equivalent ordinal notation systems in cubical Agda FN Forsberg, C Xu, N Ghani Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020 | 12 | 2020 |

Universes in sheaf models C Xu, M Escardó Unpublished note, 76, 2016 | 10 | 2016 |

Connecting constructive notions of ordinals in homotopy type theory N Kraus, FN Forsberg, C Xu arXiv preprint arXiv:2104.02549, 2021 | 9 | 2021 |

Negative consistent axioms can be postulated without loss of canonicity T Coquand, NA Danielsson, MH Escardó, U Norell, C Xu Unpublished note, 2013 | 5 | 2013 |

Type-theoretic approaches to ordinals N Kraus, FN Forsberg, C Xu Theoretical Computer Science 957, 113843, 2023 | 4 | 2023 |

Extracting the computational content of Nonstandard Analysis C Xu, S Sanders preparation; Agda code: http://cj-xu. github. io/agda/dialectica/Dialectica …, 2015 | 4 | 2015 |

A syntactic approach to continuity of T-definable functionals C Xu Logical Methods in Computer Science 16, 2020 | 3 | 2020 |

Set-theoretic and type-theoretic ordinals coincide T de Jong, N Kraus, FN Forsberg, C Xu arXiv preprint arXiv:2301.10696, 2023 | 2 | 2023 |

Type-based enforcement of infinitary trace properties for Java S Erbatur, U Schöpp, C Xu 23rd International Symposium on Principles and Practice of Declarative …, 2021 | 2 | 2021 |

A generic type system for featherweight Java U Schöpp, C Xu Proceedings of the 23rd ACM International Workshop on Formal Techniques for …, 2021 | 1 | 2021 |

A Gentzen-style monadic translation of G\" odel's System T C Xu arXiv preprint arXiv:1908.05979, 2019 | 1 | 2019 |

The ordinals in set theory and type theory are the same T de Jong, N Kraus, FN Forsberg, C Xu 29th International Conference on Types for Proofs and Programs TYPES 2023 …, 2023 | | 2023 |

Specifying a Usage Control System U Schöpp, C Xu, A Ibrahim, F Faghih, T Dimitrakos Proceedings of the 28th ACM Symposium on Access Control Models and …, 2023 | | 2023 |

Relating ordinals in set theory to ordinals in type theory T de Jong, N Kraus, FN Forsberg, C Xu | | 2023 |

Inferring Region Types via an Abstract Notion of Environment Transformation U Schöpp, C Xu Asian Symposium on Programming Languages and Systems, 45-64, 2022 | | 2022 |

On the Herbrand functional interpretation P Oliva, C Xu Mathematical Logic Quarterly 66 (1), 91-98, 2020 | | 2020 |