I am a postdoctoral member of School of Mathematics at Institute for Advanced Study. In 2017, I obtained my Ph.D. degree in Computer Science at Carnegie Mellon, with Robert Harper being my wonderful advisor.

My research ranges from programming languages to theorem proving, and I am currently focusing on mechanization of mathematics, trying to filfull part of Vladimir Voevodsky's dream. I deeply care about correctness and accuracy, and would like to improve the theory and tools to obtain higher confidence in software, hardware and mathematical proofs.

- FAVONIA at GMAIL.
- ORCID: 0000-0002-2310-3673

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

works best in LaTeX, BibTeX and Biber.

Here is my CV containing links to papers and talks.

- Mechanized reasoning in mathematics

There have been many embarrassing moments in the history of mathematics where a published proof remained unchallenged for years till it was found false. I believe most of them could have been avoided if the proofs were checked by computers; in fact, this technology has been employed in software and hardware developments to avoid bugs. However, mechanization as a practice was never widely appreciated in the community of mathematicians, possibly because of the lack of good abstraction in the current systems. I would like to improve the situation so that more people can enjoy the benefits of this technology.

- Higher-dimensional type theory

What if types also track the relations between their elements? For example, a quotient type can be viewed as the underlying set equipped with the quotient relation. I believe they can facilitate mechanization of many things. See my thesis and our codebase for my experiments in homotopy theory.

Currently I am working with Carlo Angiuli, Evan Cavallo, Robert Harper and Jonathan Sterling on

computational higher-dimensional type theory, which is inspired by the further developments of the type theory used in my thesis work, but differs significantly in details. Check out this POPL paper for an introduction, this arXiv preprint for technical details, and the proof assistant RedPRL for an implementation.

- Syntactical logical relations

These logical relations pave the way for reasoning about programming languages directly through their operational semantics. I am interested in developing these syntactical methods and applying them to practical programming problems (for example, testing).

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 (U.S.) English it might be written as
*Favonia*(capitalized) and the first syllable might reduce to a schwa. (cf.*favonian*.) - 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 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*.

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

Minimalism with GitHub-like CSS (licensed under MIT and modified by me).