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

- FAVONIA at CMU dot EDU.
- ORCID: 0000-0002-2310-3673

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

works best in LaTeX, BibTeX and Biber.

I passed my oral defense! Here is my thesis Higher-Dimensional Types in the Mechanization of Homotopy Theory. (The repository on Figshare is not set up yet due to unsolved copyright issues regarding releasing an image of a virtual machine, but in the meanwhile you can check the one on GitHub.)

- Higher-dimensional types

Higher-dimensionaltypes are types equipped with a hierarchy of relationships. Quotient types, for example, have the quotient relation as its first relation. The second relation will be among proofs of the first relation, and so on. I believe they facilitate mechanization of mathematics in general.

Currently I am focusing on the mechanization of homotopy theory and cohomology theory in the proof assistant Agda. Check our current, shared Agda codebase for my latest work. For a more general introduction, see homotopytypetheory.org. My past work includes covering spaces with Robert Harper, the Seifert-van Kampen theorem with Michael Shulman, and the Blakers-Massey theorem with Eric Finster, Peter LeFanu Lumsdaine and Dan Licata. See papers and talks for publications and slides.

- Syntactical logical relations

Syntactical logical relations pave the way to reason about programming languages directly through their operational semantics. I believe this methodology is still underdeveloped compared to denotational semantics and I would like to explore it more.

- Logic programming for social networking sites
*with Jeannette Wing*

Privacy has become an important issue for social networking sites, as users are worrying about their information shared on-line. One way to capture the concept of privacy is through epistemic logic systems, which can express that an agent may know a particular piece of information. An important aspect of privacy is to understand who knows what information, which reduces to determine whether such epistemic expressions are provable in logic systems. Inspired by the need to verify privacy specifications in social networking sites, I have designed a logic programming language with sound and complete semantics with respect to previous logic programming languages.

Covering Spaces in Homotopy Type Theory

*with Robert Harper*.

In preparation.Correctness of Compiling Polymorphism to Dynamic Typing

*with Nick Benton and Robert Harper*.

[JFP] [draft]The Seifert–van Kampen Theorem in Homotopy Type Theory

*with Michael Shulman*.

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

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

[LICS 2016 proceeding] [arXiv] [draft]A Note on the Uniform Kan Condition in Nominal Cubical Sets

*with Robert Harper*.

[arXiv]

Cohomology: Cellular and Eilenberg-Steenrod

*at*MURI grant meeting 2017

[slides] [PDF slides]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 names in everyday life are 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 names is west wind. You are welcome to pronounce them in any reasonable language, dialect or accent. You can also transliterate 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).