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

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.

I found `Kuen-Bang {Hou (Favonia)}`

works best in LaTeX, BibTeX and Biber.

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.

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.

Stay tuned!

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!

- In the United States English and British English it might be written as
*Favonia*and the first syllable might reduce to a schwa. (cf.*favonian*.) It is difficult to collect data because everyone who knows me just copies my pronunciation in English now. - In Tâi-bân it might be written as
*西風*,*Se-hong*,*Sai-hong*,*セエホン*or*サイホン*and be pronounced as*Se-hong*or*Sai-hong*. - In Bokmål it might be written as
*Favonia*, and in Norsk a possible pronunciation among so many dialects delivers the second vowel as the close back rounded vowel. - In Japanese it might be written as
*西風*,*ファボーニア*or*ファヴォーニア*and can be pronounced in many ways, including*せいふう (seifuu)*,*せいかぜ (seikaze)*(rare),*にしかぜ (nishikaze)*,*ファボーニア (fabōnia)*and*ファヴォーニア (favōnia)*. - In Mandarin it might be written as
*西風*or*西风*and be pronounced as*ㄒㄧ ㄈㄥ*or*Xīfēng*.

See also:

- Word of the Day of Merriam-Webster on 2015/12/27 [web page]
- Word of the Day of Diction.com on 2007/01/03 [web page]

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

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).