I am a postdoc in Computer Science Department at Carnegie Mellon, currently working on higher-dimensional types and random topics in programming language theory under the supervision of Robert Harper.

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

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

works best in LaTeX, BibTeX and Biber.

- Higher-dimensional types

What if types are equipped with a hierarchy of relationships on top of their elements? I think they can facilitate mechanization of many things! See my thesis and our codebase for my experiments in homotopy theory.

- Syntactical logical relations

These logical relations pave the way to reason about programming languages directly through their operational semantics.

Covering Spaces in Homotopy Type Theory

*with Robert Harper*.

In preparation.Higher-Dimensional Types in the Mechanization of Homotopy Theory (Ph.D. Thesis)

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]

Compiling Polymorphism to Dynamic Typing

*at*PLunch 2017/04/07

[slides] [PDF slides]Axiomatic and cellular cohomology theory

*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!

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