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:

- In the United States (U.S.) English it is probably written as
*Favonia*(capitalized), and the first syllable probably reduces to a schwa. (cf.*favonian*.) - In Tâi-bân it is probably written as
*西風*,*Se-hong*,*Sai-hong*,*セエ ホン*or*サイ ホン*, and is probably pronounced as*Se-hong*or*Sai-hong*. - In Japanese it is probably written as
*西風*,*ファボーニア*or*ファヴォーニア*, and could be pronounced in many ways, including*せいふう (seifuu)*,*せいかぜ (seikaze)*,*にしかぜ (nishikaze)*,*ファボーニア (fabōnia)*and*ファヴォーニア (favōnia)*.

- Higher-dimensional Types
*with Robert Harper and many others*

A

higher-dimensionaltype, 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.)

- Homotopy Theory in Type Theory

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.

- 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.
- Teaching Assistant of 15210: Parallel and Sequential Data Structures and Algorithms, Fall 2015.