[papers] [talks] [artifacts] [thesis] [CV]

A profile picture of Favonia standing on the rocks, facing backwards. I am an assistant professor at the University of Minnesota. My research interests lie in achieving a high level of rigor in computer programs and mathematical proofs. In particular, I have been working on proof mechanization, type theory, compiler correctness and property-based testing.


How to Cite My Name in Your LaTeX Papers

I found Kuen-Bang {Hou (Favonia)} works best in LaTeX, BibTeX and Biber.


Mechanized Reasoning in Mathematics

I believe the primary reason why most mathematicians remain unfamiliar with mechanical verification is the fear of length and complexity of mechanized proofs, and this can be addressed by a good abstraction language such as type theory, which should match conventional mathematics while fulfilling the need of mechanical checking.

I have been collaborating with others to mechanize theorems in homotopy theory (see my papers and our Agda code) through a new type theory—homotopy type theory. This new type theory came from a surprising connection between dependent type theory and homotopy theory; it reveals higher-dimensional structures in dependent type theories that naturally represent the higher-dimensional structures in homotopy theory.

To see how the new type theory addresses mathematicians’ concerns, our mechanized proofs do not seem longer or more complicated than the proofs in standard textbooks; moreover, the system is friendly enough that some of us even start proving theorems directly in computers. There were cases where a traditionally trained mathematician learned to read our mechanized proofs in a short time. Our results even inspired new development in mathematics: we not only verified known results but also provided new insights.

Cubical Computational Type Theory

Another thread of my research is to extend other type theories with higher-dimensional structures inspired by homotopy type theory. My current target is computational type theory, exemplified by the well-known proof assistant Nuprl, where types classify programs by their computational behaviors. It had remained open whether one can extend its semantics with higher-dimensional features, and our work answered this question positively by treating each program as an n-dimensional cube. Programs in ordinary type theory may be regarded as homogeneous cubes, and new features enable the construction of heterogeneous ones. We showed these cubical structures are sufficient to justify key features of homotopy type theory. Based on the theory, we are also building proof assistants RedPRL and redtt.

Our type theory and tool not only addressed the long-standing open problem about the computational content of homotopy type theory, but also provided much stronger reasoning principles for equality than those in homotopy type theory or other variants. Moreover, it paved the way for integrating features from other programming languages such as exceptions or non-termination, going beyond the realm of verifying mathematical proofs. Research already suggested that homotopy type theory is useful for program reasoning, and ours should make an even stronger case after integrating common programming features.

Other Random Stuff

Stay tuned!

Archived Research Projects

See archived research projects.


My names in everyday life are the sequences f-a-v-o-n-i-a and 西-. My governmental name is Kuen-Bang Hou (transliteration of the Mandarin name 侯昆邦). I go by Kuen-Bang Hou (Favonia) in academics.

The meaning of my everyday names is west wind. You are welcome to pronounce them in any reasonable language, dialect or accent. You can also transliterate them into any reasonable writing system. Please share with me your pronunciation and/or transcription!

See also:


I go by singular they but people often choose he because of my perceived gender.

Knuth’s Check

I am aware that Knuth wanted to send me a check, but I was not unable to reach them (Knuth or Knuth’s secretary) through emails.

This page was made with GitHub-like CSS (licensed under MIT and modified by me).