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.


My name at CMU. No Andrew.


  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. See homotopytypetheory.org for more information. Here are specific documents:

  1. Correctness through 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. So far I found Kuen-Bang {Hou (Favonia)} works best for BibLaTeX+Biber.

The meaning 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. For example:

Please share with me your pronunciation and/or transcription. I am eager to learn!

This Page

Extreme minimalism.