Favonia (Kuen-Bang Hou)

A profile picture of Favonia in a red shirt. I am a postdoctoral member of School of Mathematics at Institute for Advanced Study. In 2017, I obtained my Ph.D. degree in Computer Science at Carnegie Mellon, with Robert Harper being my wonderful advisor. Here is my thesis.

My research interests lie in using type theory to achieve a higher level of rigor in computer programs and mathematical proofs. In particular, I have been working on mechanization of mathematical proofs, proof assistants, computational type theory, compiler correctness and property-based testing. Check out my CV which lists my papers and my talks.

I will be joining University of Minnesota in Fall 2018!

Contact

How to Cite My Name in Your LaTeX Papers

I found Kuen-Bang {Hou (Favonia)} works best in LaTeX, BibTeX and Biber.

Current Research

Mechanized reasoning in mathematics

Despite the usefulness of mechanical verification in computer science, most mathematicians remain unfamiliar with this technology. I believe this is due to the fear of length and complexity of mechanized proofs, and can be addressed by a good abstraction language such as type theory, which should match conventional mathematics while fulfilling the need of mechanical checking.

In the recent years, I have been collaborating with others to mechanize several important theorems in homotopy theory (see my thesis, my papers or our Agda code) through a new type theory—homotopy type theory. This new type theory came from a surprising connection between dependent type theory and homotopy theory; it reveals higher-dimensional structures in dependent type theories that naturally represent the higher-dimensional structures in homotopy theory.

To see how the new type theory addresses mathematicians’ concerns, our mechanized proofs do not seem longer or more complicated than the proofs in textbooks; moreover, the system is friendly enough that some of us even start proving theorems directly in computers. There were cases where a traditionally trained mathematician learned to read our mechanized proofs in a short time. Our results even inspired new development in mathematics: we not only verified known results but also provided new insights.

Cubical Computational Type Theory

Another thread of my research is to extend other type theories with higher-dimensional (for example cubical) structures inspired by homotopy type theory. My current target is computational type theory, exemplified by the well-known proof assistant Nuprl, where types classify programs by their computational behaviors. It had remained open whether one can extend its semantics with higher-dimensional features, and my joint work with Carlo Angiuli, Evan Cavallo, Robert Harper, Jonathan Sterling and Todd Wilson answered this question positively by treating each program as an n-dimensional cube. Programs in ordinary type theory may be regarded as homogeneous cubes, and new features enable the construction of heterogeneous ones. We showed these cubical structures are sufficient to justify key features of homotopy type theory. Based on the theory, we are also building the proof assistant RedPRL with a new design of dependent refinement logic.

Our type theory and tool not only addressed the long-standing open problem about the computational content of homotopy type theory, but also provided much stronger reasoning principles for equality than those in homotopy type theory or other variants. Moreover, it paved the way for integrating features from other programming languages such as exceptions or concurrency, going beyond the realm of verifying mathematical proofs. Research already suggested that homotopy type theory is useful for program reasoning, and ours should make an even stronger case after integrating common programming features.

Reasoning with Logical Relations

Logical relations assign to each type a meaning reflecting its logical structure, and is one of the most important methods for proving program equivalence, non-interference, termination and various properties. Nick Benton, Robert Harper and I managed to prove the correctness of compiling polymorphism of System F to dynamic typing through a modified cross-language logical relation. In fact, the computational type theory mentioned above can also be regarded as a logical relation on untyped lambda calculus. In the future, I would like to explore other applications of logical relations and build tools to help programmers.

Name

My names in everyday life are the sequences f-a-v-o-n-i-a and 西-. My governmental name is Kuen-Bang Hou (transliteration of the Mandarin name 侯昆邦). 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!

Pronoun

I go by singular they but people often choose he because of my perceived gender.

Knuth’s Check

I am aware that Knuth wanted to send me a check, but I was not unable to reach them (Knuth or Knuth’s secretary) through emails.


This page was made with GitHub-like CSS (licensed under MIT and modified by me).