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.

This page is intentionally simple-formatted as a lazy accessibility solution.


My name at CMU. No Andrew.


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:

Research Projects

  1. Higher-dimensional Types with Robert Harper and many others

A higher-dimensional type, in my definition, is a type equipped with a relationship between terms, and possibly a relationship between two proofs relating two terms, and so on. (Note that this terminology is not widely-accepted yet.)

One popular research direction is to represent higher-dimensional structures in topological spaces as those in types. Check the HoTT book, this resourceful website and this wiki.

I have been involved in mechanization following this trend. See our new codebase and my old codebase for my work in the proof assistant Agda.

Talk at TYPES 2014: the SVG slides, their PDF export and the PDF abstract draft.

Talk at CHomotopy 2013: the SVG slides, their PDF export. and the PDF abstract draft.

  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.

  1. Type refinements with Robert Harper

Types (in the Church style) are ontological classifications of terms defined before operational semantics, where refinements are mathematical properties of terms defined after. We demonstrated that refinements are useful in proving correctness of compilers by capturing compilation invariants in target languages.

This is also the first known correctness proof of compiling System F polymorphism to dynamic typing.