Kuen-Bang Hou (Favonia)


I am a postdoctoral member of School of Mathematics at Institute for Advanced Study. My research ranges from programming languages to theorem proving, and I am currently working on mechanized reasoning under the supervision of Vladimir Voevodsky. I deeply care about correctness and accuracy, and would like to improve our theoretical foundations and practical tools to obtain higher confidence in software, hardware and mathematical proofs.

I obtained my Ph.D. degree in Computer Science at Carnegie Mellon, with Robert Harper being my wonderful advisor.


How to Cite My Name in Your LaTeX Papers

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

Current Research

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

  1. Higher-dimensional type theory

What if types are equipped with a hierarchy of relationships on top of 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. See this POPL paper for an introduction.

  1. 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. 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!


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

This Page

Minimalism with GitHub-like CSS (licensed under MIT).