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 | 51 | 2015 |
A constructive model of uniform continuity C Xu, M Escardó Typed Lambda Calculi and Applications: 11th International Conference, TLCA …, 2013 | 27 | 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 | 22 | 2016 |
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 | 16 | 2020 |
A continuous computational interpretation of type theories C Xu University of Birmingham, 2015 | 15 | 2015 |
Set-theoretic and type-theoretic ordinals coincide T de Jong, N Kraus, FN Forsberg, C Xu 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1-13, 2023 | 11 | 2023 |
Connecting constructive notions of ordinals in homotopy type theory N Kraus, FN Forsberg, C Xu arXiv preprint arXiv:2104.02549, 2021 | 10 | 2021 |
Universes in sheaf models C Xu, M Escardó Unpublished note, 76, 2016 | 10 | 2016 |
Type-theoretic approaches to ordinals N Kraus, FN Forsberg, C Xu Theoretical Computer Science 957, 113843, 2023 | 9 | 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 | 5 | 2023 |
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 |
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 |
Type-based enforcement of infinitary trace properties for Java S Erbatur, U Schöpp, C Xu Proceedings of the 23rd International Symposium on Principles and Practice …, 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 | 2 | 2021 |
A Gentzen-style monadic translation of G\" odel's System T C Xu arXiv preprint arXiv:1908.05979, 2019 | 1 | 2019 |
Ordinal exponentiation in homotopy type theory T de Jong, N Kraus, FN Forsberg, C Xu arXiv preprint arXiv:2501.14542, 2025 | | 2025 |
Static and Dynamic Analysis of a Usage Control System U Schöpp, F Faghih, S Bandopadhyay, H Joumaa, A Ibrahim, C Xu, X Ye, ... Proceedings of the 29th ACM Symposium on Access Control Models and …, 2024 | | 2024 |
Constructive Ordinal Exponentiation in Homotopy Type Theory T de Jong, N Kraus, FN Forsberg, C Xu 30th International Conference on Types for Proofs and Programs TYPES 2024 …, 2024 | | 2024 |
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 |