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.

- 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-dimensionaltype 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 relationshipshigher-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.

- Covering spaces
with Robert Harper

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.

- 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.

- Type refinements
*with Robert Harper*

Types (in the Church style) are ontological classifications of terms defined

beforeoperational semantics, where refinements are mathematical properties of terms definedafter. 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.

- Type Refinements for Compiler Correctness
with Robert Harper. The PDF draft and the full proof in PDF.

- Logic systems for computer scientists at FLOLAC 2012. The SVG slides and the PDF export in Mandarin.

- Teaching Assistant of 15814: Type Systems for Programming Languages, Fall 2012.