| Syntax and models of Cartesian cubical type theory C Angiuli, G Brunerie, T Coquand, R Harper, KB Hou, DR Licata Mathematical Structures in Computer Science 31 (4), 424-468, 2021 | 63* | 2021 |
| Cartesian cubical computational type theory: Constructive reasoning with paths and equalities C Angiuli, KBF Hou, R Harper Computer Science Logic 2018, 2018 | 58 | 2018 |
| A mechanization of the Blakers-Massey connectivity theorem in homotopy type theory KB Hou, E Finster, DR Licata, PLF Lumsdaine Proceedings of the 31st annual ACM/IEEE symposium on logic in computer …, 2016 | 43 | 2016 |
| Cellular cohomology in homotopy type theory U Buchholtz, KB Hou Favonia Proceedings of the 33rd annual acm/ieee symposium on logic in computer …, 2018 | 29 | 2018 |
| The Seifert-van Kampen theorem in homotopy type theory M Shulman 25th eacsl annual conference on computer science logic (csl 2016), 2016 | 23 | 2016 |
| Computational higher type theory III: Univalent universes and exact equality C Angiuli, KB Hou, R Harper arXiv preprint arXiv:1712.01800, 2017 | 16* | 2017 |
| Evan Cavallo, Tim Baumann, Eric Finster, Jesper Cockx, Christian Sattler, Chris Jeris, Michael Shulman, et al G Brunerie, KB Hou Homotopy type theory in Agda, 2021 | 15 | 2021 |
| Higher-Dimensional Types in the Mechanization of Homotopy Theory. KB Hou Carnegie Mellon University, USA, 2017 | 11 | 2017 |
| The RedPRL proof assistant C Angiuli, E Cavallo, KB Hou, R Harper, J Sterling arXiv preprint arXiv:1807.01869, 2018 | 10 | 2018 |
| Correctness of compiling polymorphism to dynamic typing KB Hou, N Benton, R Harper Journal of Functional Programming 27, e1, 2017 | 9 | 2017 |
| Covering Spaces in Homotopy Type Theory R Harper 22nd International Conference on Types for Proofs and Programs (TYPES 2016), 2018 | 8 | 2018 |
| Covering spaces in homotopy type theory KB Hou Extended Abstracts Fall 2013: Geometrical Analysis; Type Theory, Homotopy …, 2015 | 8 | 2015 |
| Evan Cavallo, Tim Baumann, Eric Finster, Jesper Cockx, Christian Sattler, Chris Jeris, Michael Shulman, et al. Homotopy Type Theory in Agda. 2018 G Brunerie, KB Hou | 6 | |
| and Robert Harper C Angiuli, KB Hou Computational higher type theory III: Univalent universes and exact equality, 2017 | 5 | 2017 |
| An Order-Theoretic Analysis of Universe Polymorphism KB Hou, C Angiuli, R Mullanix Proceedings of the ACM on Programming Languages 7 (POPL), 1659-1685, 2023 | 4 | 2023 |
| Logarithm and program testing KB Hou, Z Wang Proceedings of the ACM on Programming Languages 6 (POPL), 1-26, 2022 | 4 | 2022 |
| & Robert Harper (2017): Computational Higher Type Theory III: Univalent Universes and Exact Equality C Angiuli, KB Hou arXiv preprint cs.LO/1712.01800, 0 | 4 | |
| A Note on the Uniform Kan Condition in Nominal Cubical Sets R Harper, KB Hou arXiv preprint arXiv:1501.05691, 2015 | 3 | 2015 |
| Homotopy Type Theory: Univalent Foundations of Mathematics P Aczel, B Ahrens, T Altenkirch, S Awodey, B Barras, A Bauer, Y Bertot, ... Aucun, 2013 | 2 | 2013 |
| Coslice Colimits in Homotopy Type Theory P Hart, KB Hou arXiv preprint arXiv:2411.15103, 2024 | | 2024 |
Carlo AngiuliAssistant Professor, Indiana UniversityVerified email at indiana.edu
