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.

This page is intentionally ugly as a simple accessibility solution.

- Higher type theory

Higher type theoryis the study of higher-structural types.

Traditionally, a type defines a collection of terms and their interface. (See the discussion of refinements below.) Higher-structural types additionally are equipped with a relationship between terms, and possibly a relationship between relationships, and so on. For example, a quotient type may be thought as the underlying type plus an equivalence relationship. I call these relationships

higher structures, and thus the namehighertype theory.

One popular research direction is based on modeling paths in homotopy theory by (equivalence) relationships. For more information about this direction, please check this resourceful website and this wiki. Yes, there is even a book. I have been involved in mechanization of many type-theoretical proofs inspired by homotopy theory. See our new codebase and my old codebase about mechanization of homotopy-theoretical proofs in Agda. The following are some talks and writings about parts of my work.

- Covering spaces
with Robert Harper

Talk at TYPES 2014: the SVG slides, their PDF export and the PDF abstract draft.

Talk at CHomotopy 2013: the SVG slides, their PDF export. and the PDF abstract draft.

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

- Type refinements
*with Robert Harper*

Types are ontological classifications of terms defined

beforeoperational semantics, where refinements are mathematical properties of terms definedafter. Refinements were called “types” in various theories based on operational semantics, but we would like to have two different names for these two different concepts. We demonstrate that refinements are useful in proving correctness of compilers for compilation invariants could potentially be captured by refinements in target languages.

- Type Refinements for Compiler Correctness
with Robert Harper. The PDF draft and the full proof in PDF.

We gave the first correctness proof of compiling System F polymorphism to dynamic typing.

- Logic systems for computer scientists at FLOLAC 2012. The SVG slides and the PDF export in Mandarin.

- Teaching Assistant of 15814: Type Systems for Programming Languages, Fall 2012.

My official name on government IDs is Kuen-Bang Hou, but I prefer people calling me “favonia” (in any sensible language), thanks.