A Note on the Uniform Kan Condition in Nominal Cubical Sets. - Robert Harper 001; Kuen-Bang Hou (Favonia) (CoRR, 2015)

The Seifert-van Kampen Theorem in Homotopy Type Theory. - Kuen-Bang Hou (Favonia); Michael Shulman (CSL, 2016)

A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory. - Kuen-Bang Hou (Favonia); Eric Finster; Daniel R. Licata; Peter LeFanu Lumsdaine (LICS, 2016)

Covering Spaces in Homotopy Type Theory. - Kuen-Bang Hou (Favonia); Robert Harper 001 (TYPES, 2016)

Computational Higher Type Theory III: Univalent Universes and Exact Equality. - Carlo Angiuli; Kuen-Bang Hou (Favonia); Robert Harper 001 (CoRR, 2017)

Correctness of compiling polymorphism to dynamic typing. - Kuen-Bang Hou (Favonia); Nick Benton; Robert Harper 001 (J. Funct. Program., 2017)

Higher-Dimensional Types in the Mechanization of Homotopy Theory. - Kuen-Bang Hou (Favonia) (2017)

Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities. - Carlo Angiuli; Kuen-Bang Hou (Favonia); Robert Harper 001 (CSL, 2018)

The RedPRL Proof Assistant (Invited Paper). - Carlo Angiuli; Evan Cavallo; Kuen-Bang Hou (Favonia); Robert Harper 001; Jonathan Sterling (LFMTP@FSCD, 2018)

Cellular Cohomology in Homotopy Type Theory. - Ulrik Buchholtz; Kuen-Bang Hou (Favonia) (Log. Methods Comput. Sci., 2020)

Syntax and models of Cartesian cubical type theory. - Carlo Angiuli; Guillaume Brunerie; Thierry Coquand; Robert Harper 001; Kuen-Bang Hou (Favonia); Daniel R. Licata (Math. Struct. Comput. Sci., 2021)

Logarithm and program testing. - Kuen-Bang Hou (Favonia); Zhuyang Wang (Proc. ACM Program. Lang., 2022)

An Order-Theoretic Analysis of Universe Polymorphism. - Kuen-Bang Hou (Favonia); Carlo Angiuli; Reed Mullanix (Proc. ACM Program. Lang., 2023)

Coslice Colimits in Homotopy Type Theory. - Perry Hart; Kuen-Bang Hou (Favonia) (CSL, 2025)