| Syntax and Models of Cartesian Cubical Type Theory C Angiuli, G Brunerie, T Coquand, KB Hou, R Harper, DR Licata Mathematical Structures in Computer Science 31 (4), 424-468, 2021 | 62* | 2021 |
| Normalization for cubical type theory J Sterling, C Angiuli LICS 2021 (36th Annual ACM/IEEE Symposium on Logic in Computer Science), 2021 | 60 | 2021 |
| Cartesian cubical computational type theory: Constructive reasoning with paths and equalities C Angiuli, KB Hou, R Harper CSL 2018 (27th EACSL Annual Conference on Computer Science Logic), 2018 | 59 | 2018 |
| Computational higher-dimensional type theory C Angiuli, R Harper, T Wilson POPL 2017 (44th ACM SIGPLAN Symposium on Principles of Programming Languages …, 2017 | 55 | 2017 |
| Homotopical patch theory C Angiuli, E Morehouse, DR Licata, R Harper ICFP 2014 (19th ACM SIGPLAN International Conference on Functional …, 2014 | 42 | 2014 |
| Internalizing representation independence with univalence C Angiuli, E Cavallo, A Mörtberg, M Zeuner POPL 2021 (48th ACM SIGPLAN Symposium on Principles of Programming Languages), 2021 | 39 | 2021 |
| Cubical syntax for reflection-free extensional equality J Sterling, C Angiuli, D Gratzer FSCD 2019 (4th International Conference on Formal Structures for Computation …, 2019 | 31 | 2019 |
| Computational semantics of Cartesian cubical type theory C Angiuli PhD thesis. Pittsburgh, PA, USA: Carnegie Mellon University, 2019 | 29 | 2019 |
| Computational higher type theory I: Abstract cubical realizability C Angiuli, R Harper, T Wilson arXiv preprint arXiv:1604.08873, 2016 | 24 | 2016 |
| The RedPRL proof assistant C Angiuli, E Cavallo, KB Hou, R Harper, J Sterling LFMTP 2018 (13th International Workshop on Logical Frameworks and Meta …, 2018 | 21* | 2018 |
| Computational higher type theory III: Univalent universes and exact equality C Angiuli, KB Hou, R Harper arXiv preprint arXiv:1712.01800, 2017 | 21* | 2017 |
| A cubical language for Bishop sets J Sterling, C Angiuli, D Gratzer Logical Methods in Computer Science 18 (1), 2022 | 19 | 2022 |
| Computational higher type theory II: Dependent cubical realizability C Angiuli, R Harper arXiv preprint arXiv:1606.09638, 2016 | 17 | 2016 |
| Meaning explanations at higher dimension C Angiuli, R Harper Indagationes Mathematicae 29 (1), 135-149, 2018 | 13 | 2018 |
| Homotopical patch theory C Angiuli, E Morehouse, DR Licata, R Harper Journal of Functional Programming 26, e18, 2016 | 13 | 2016 |
| Automatically splitting a two-stage lambda calculus N Feltman, C Angiuli, UA Acar, K Fatahalian ESOP 2016 (25th European Symposium on Programming), 255-281, 2016 | 11 | 2016 |
| Controlling unfolding in type theory D Gratzer, J Sterling, C Angiuli, T Coquand, L Birkedal arXiv preprint arXiv:2210.05420, 2022 | 6 | 2022 |
| An Order-Theoretic Analysis of Universe Polymorphism KB Hou, C Angiuli, R Mullanix POPL 2023 (50th ACM SIGPLAN Symposium on Principles of Programming Languages), 2023 | 4 | 2023 |
| Gluing models of type theory along flat functors J Sterling, C Angiuli Unpublished manuscript, 2020 | 4 | 2020 |
| The (∞, 1)-accidentopos model of unintentional type theory C Angiuli Sigbovik, 2013 | 3 | 2013 |
Kuen-Bang Hou (Favonia)University of Minnesota, Twin CitiesVerified email at umn.edu
