I am a postdoctoral member of School of Mathematics at Institute for Advanced Study. My research ranges from programming languages to theorem proving, and I am currently working on mechanized reasoning under the supervision of Vladimir Voevodsky. I deeply care about correctness and accuracy, and would like to improve our theoretical foundations and practical tools to obtain higher confidence in software, hardware and mathematical proofs.

I obtained my Ph.D. degree in Computer Science at Carnegie Mellon, with Robert Harper being my wonderful advisor.

- FAVONIA at GMAIL.
- ORCID: 0000-0002-2310-3673

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

works best in LaTeX, BibTeX and Biber.

- Mechanized reasoning in mathematics

There have been many embarrassing moments in the history of mathematics where a published proof remained unchallenged for years till it was found false. I believe most of them could have been avoided if the proofs were checked by computers; in fact, this technology has been employed in software and hardware developments to avoid bugs. However, mechanization as a practice was never widely appreciated in the community of mathematicians, possibly because of the lack of good abstraction in the current systems. I would like to improve the situation so that more people can enjoy the benefits of this technology.

- Higher-dimensional type theory

What if types are equipped with a hierarchy of relationships on top of their elements? For example, a quotient type can be viewed as the underlying set equipped with the quotient relation. I believe they can facilitate mechanization of many things. See my thesis and our codebase for my experiments in homotopy theory.

Currently I am working with Carlo Angiuli, Evan Cavallo, Robert Harper and Jonathan Sterling on

computational higher-dimensional type theory, which is inspired by the further developments of the type theory used in my thesis work, but differs significantly in details. See this POPL paper for an introduction.

- Syntactical logical relations

These logical relations pave the way for reasoning about programming languages directly through their operational semantics. I am interested in developing these syntactical methods and applying them to practical programming problems (for example, testing).

Covering Spaces in Homotopy Type Theory

*with Robert Harper*.

[draft] (submitted to the TYPES 2016 post-proceedings)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]

Homotopy Type Theory in Agda

*at*Big Proof 2017/07/07

[slides]Computational Higher-Dimensional Type Theory

*at*Big Proof 2017/07/04

[slides]Compiling Polymorphism to Dynamic Typing

*at*PLunch 2017/04/07

[slides]Axiomatic and cellular cohomology theory

*at*MURI grant meeting 2017

[slides]The Seifert-van Kampen Theorem in Homotopy Type Theory

*at*CSL 2016

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

*at*LICS 2016

[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] [recording]Covering Spaces in Homotopy Type Theory

*at*TYPES 2014

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

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

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

*at*FLOLAC 2012

[slides]

- Member of ICFP 2017 Artifact Evaluation Committee

- Teaching Assistant of CMU 15-814: Type Systems for Programming Languages, Fall 2012
- Teaching Assistant of CMU 15-210: 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).