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. I was an undergraduate at National Taiwan University and a research assistant at Academia Sinica (in Taiwan).

- My everyday name at CMU dot EDU. No ANDREW.
- ORCID: 0000-0002-2310-3673

I found `Kuen-Bang {Hou (Favonia)}`

works best for BibLaTeX+Biber.

- Higher-dimensional types

A

higher-dimensionaltype 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:

- My thesis proposal (updated after the proposal)
- Our shared Agda codebase
- My old Agda codebase (abandoned)
- Covering Spaces in Homotopy Type Theory
with Robert Harper- The Seifert–van Kampen Theorem in Homotopy Type Theory
with Michael Shulman.Accepted by CSL 2016.[draft]- A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory
with Eric Finster, Peter LeFanu Lumsdaine and Dan Licata.To appear in the LICS 2016 proceeding.[arXiv] [draft]- A Note on the Uniform Kan Condition in Nominal Cubical Sets
with Robert Harper. [arXiv]

- Logical relations

Logical relations are powerful in proving correctness. Here are specific papers:

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

A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory

*at*LICS 2016

[slides] [PDF slides (the title was rendered broken)]Seifert-van Kampen Theorem in Homotopy Type Theory

*at*Workshop on Homotopy Type Theory and Univalent Foundations of Mathematics (2016)

[slides] [recording]Covering Spaces in Homotopy Type Theory

*at*TYPES 2014

[slides] [PDF slides] [abstract draft]Covering Spaces in Homotopy Type Theory

*at*Conference on Type Theory, Homotopy Theory and Univalent Foundations (2013)

[slides] [PDF slides] [abstract] [abstract draft]給電腦科學家的邏輯系統 (Logic Systems for Computer Scientists)

*at*FLOLAC 2012

[slides] [PDF slides]

- Teaching Assistant of 15814: Type Systems for Programming Languages, Fall 2012
- Teaching Assistant of 15210: Parallel and Sequential Data Structures and Algorithms, Fall 2015

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.

The meaning of my everyday name 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. Please share with me your pronunciation and/or transcription. I am eager to learn!

- 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)*(rare),*にしかぜ (nishikaze)*,*ファボーニア (fabōnia)*and*ファヴォーニア (favōnia)*. - In Mandarin it is probably written as
*西風*or*西风*and is pronounced as*ㄒㄧ ㄈㄥ*or*Xīfēng*.

I prefer *singular they* but people often choose *he* because of my perceived gender.

Minimalism with GitHub-like CSS (licensed under MIT).