favonia 西風 Sai-hong


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 for BibLaTeX+Biber.


See Papers for my published works. This section is a brief description of my research.

  1. Higher-dimensional types

A higher-dimensional type is a type equipped with a hierarchy of relationships. I believe they facilitate mechanization in general, but my current focus is homotopy theory. The following two references give all the details:

See homotopytypetheory.org for more information about this new area.

My past works:

  1. Logical relations

Logical relations are powerful in proving correctness. Here are specific papers:

  1. Logic programming for social networking sites with Jeannette Wing

This project is to design a logic programming language inspired by verification of social networking sites.





My name in everyday life is 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 name is west wind. You are welcome to pronounce them in any reasonable language, dialect or accent. You can also transcribe 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).