Kuen-Bang Hou (Favonia)


I am a Ph.D. student in Computer Science Department at Carnegie Mellon, currently working on logic and programming language theory under the supervision of Robert Harper. I was previously advised by Jeannette Wing and Avrim Blum for research in privacy. I was an undergraduate at National Taiwan University and a research assistant at Academia Sinica (in Taiwan).


How to Cite My Name in Your LaTeX Papers

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


I passed my oral defense! Here is my thesis Higher-Dimensional Types in the Mechanization of Homotopy Theory. (The repository on Figshare is not set up yet due to unsolved copyright issues regarding releasing an image of a virtual machine, but in the meanwhile you can check the one on GitHub.)


  1. Higher-dimensional types

Higher-dimensional types are types equipped with a hierarchy of relationships. Quotient types, for example, have the quotient relation as its first relation. The second relation will be among proofs of the first relation, and so on. I believe they facilitate mechanization of mathematics in general.

Currently I am focusing on the mechanization of homotopy theory and cohomology theory in the proof assistant Agda. Check our current, shared Agda codebase for my latest work. For a more general introduction, see homotopytypetheory.org. My past work includes covering spaces with Robert Harper, the Seifert-van Kampen theorem with Michael Shulman, and the Blakers-Massey theorem with Eric Finster, Peter LeFanu Lumsdaine and Dan Licata. See papers and talks for publications and slides.

  1. Syntactical logical relations

Syntactical logical relations pave the way to reason about programming languages directly through their operational semantics. I believe this methodology is still underdeveloped compared to denotational semantics and I would like to explore it more.

  1. Logic programming for social networking sites with Jeannette Wing

Privacy has become an important issue for social networking sites, as users are worrying about their information shared on-line. One way to capture the concept of privacy is through epistemic logic systems, which can express that an agent may know a particular piece of information. An important aspect of privacy is to understand who knows what information, which reduces to determine whether such epistemic expressions are provable in logic systems. Inspired by the need to verify privacy specifications in social networking sites, I have designed a logic programming language with sound and complete semantics with respect to previous logic programming languages.





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 am eager to learn!


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

This Page

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