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.

See Papers for my published works. This section is a brief description of my research.

- 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. The following two references give all the details:

- My thesis proposal (updated after the proposal).
- Our current, shared Agda codebase.

See homotopytypetheory.org for more information about this new area.

My past works:

- Covering Spaces
with Robert Harper.- The Seifert-van Kampen Theorem
with Michael Shulman.- The Blakers-Massey Connectivity Theorem
with Eric Finster, Peter LeFanu Lumsdaine and Dan Licata.- Rephrasing Uniform Kan Condition
with Robert Harper.- My old Agda codebase (abandoned).

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

Correctness of Compiling Polymorphism to Dynamic Typing

*with Nick Benton and Robert Harper*.

[draft] (To appear as a JFP Theoretical Pearl.)The Seifert–van Kampen Theorem in Homotopy Type Theory

*with Michael Shulman*.

[draft] [CSL 2016]A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory

*with Eric Finster, Dan Licata and Peter LeFanu Lumsdaine*.

[arXiv] (To appear in LICS 2016 proceeding.)A Note on the Uniform Kan Condition in Nominal Cubical Sets

*with Robert Harper*.

[arXiv]

The Seifert-van Kampen Theorem in Homotopy Type Theory

*at*CSL 2016

[slides] [PDF slides]A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory

*at*LICS 2016

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

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

[slides] [PDF 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 might be written as
*Favonia*(capitalized) and the first syllable might reduce to a schwa. (cf.*favonian*.) - In Tâi-bân it might be written as
*西風*,*Se-hong*,*Sai-hong*,*セエホン*or*サイホン*and be pronounced as*Se-hong*or*Sai-hong*. - In Japanese it might be written as
*西風*,*ファボーニア*or*ファヴォーニア*and can be pronounced in many ways, including*せいふう (seifuu)*,*せいかぜ (seikaze)*(rare),*にしかぜ (nishikaze)*,*ファボーニア (fabōnia)*and*ファヴォーニア (favōnia)*. - In Mandarin it might be written as
*西風*or*西风*and be 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).