Kuen-Bang Hou (Favonia)

Favonia's profile 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.


How to Cite My Name in Your LaTeX Papers

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

Curriculum Vitae

Here is my CV containing links to papers and talks.

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

  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 (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!


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

This Page

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