| Cartesian cubical computational type theory: Constructive reasoning with paths and equalities C Angiuli, R Harper 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), 2018 | 46 | 2018 |
| 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 | 41* | 2021 |
| 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 | 31 | 2016 |
| The Seifert-van Kampen theorem in homotopy type theory M Shulman 25th eacsl annual conference on computer science logic (csl 2016), 2016 | 18 | 2016 |
| Evan Cavallo, Eric Finster, Jesper Cockx, Christian Sattler, Chris Jeris, Michael Shulman, et al G Brunerie, KB Hou Homotopy type theory in Agda, 2018 | 17 | 2018 |
| Computational higher type theory III: Univalent universes and exact equality C Angiuli, KB Hou, R Harper arXiv preprint arXiv:1712.01800, 2017 | 17* | 2017 |
| Cellular cohomology in homotopy type theory U Buchholtz, KB Hou Favonia Proceedings of the 33rd annual acm/ieee symposium on logic in computer …, 2018 | 16 | 2018 |
| The RedPRL proof assistant C Angiuli, E Cavallo, KB Hou, R Harper, J Sterling arXiv preprint arXiv:1807.01869, 2018 | 10 | 2018 |
| Higher-dimensional types in the mechanization of homotopy theory KB Hou US Army, 2017 | 9 | 2017 |
| 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 KB Hou Extended Abstracts Fall 2013: Geometrical Analysis; Type Theory, Homotopy …, 2015 | 8 | 2015 |
| Covering Spaces in Homotopy Type Theory R Harper 22nd International Conference on Types for Proofs and Programs (TYPES 2016), 2018 | 6 | 2018 |
| & 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 |
| Logarithm and program testing. KB Hou, Z Wang Proc. ACM Program. Lang. 6 (POPL), 1-26, 2022 | 1 | 2022 |
| 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 | | 2023 |
| Cellular Cohomology in Homotopy Type Theory KB Hou, U Buchholtz Logical Methods in Computer Science 16, 2020 | | 2020 |
| Cartesian Cubical Computational Type Theory C Angiuli, KB Hou, R Harper | | |
| Computational Cubical Type Theory KB Hou | | |
Carlo AngiuliPostdoc, Carnegie Mellon UniversityVerified email at cs.cmu.edu
