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 sequence f-a-v-o-n-i-a. You are welcome to pronounce it in any reasonable language, dialect or accent. You can also transcribe it into any reasonable writing system. For example in the United States (U.S.) English it is probably written Favonia (capitalized) and the first syllable probably reduces to a schwa. (cf. favonian.)

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.

Research Projects

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

Traditionally, a type (in the Church style) defines a collection of terms and their interface. A higher-dimensional type is additionally equipped with a relationship between terms, and probably a relationship between proofs of these relationships, and so on. I call this tower of relationships higher-dimensional structures.

One popular research direction, in retrospect, is to build higher-dimensional structures from iterated identification types, to interpret these structures in type theory into paths in homotopy theory, and to assert that equivelant things are equal (univalence). Chech the book and this resourceful website and this wiki.

I have been involved in mechanization of homotopy theory along this line. See our new codebase and my old codebase for my mechanization in Agda. The following are some talks and writings about parts of my work.

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.