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 is 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 name higher type 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.
This project is to design a logic programming language inspired by verification of social networking sites.
Types are ontological classifications of terms defined before operational semantics, where refinements are mathematical properties of terms defined after. 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.
We gave the first correctness proof of compiling System F polymorphism to dynamic typing.
My official name on government IDs is Kuen-Bang Hou, but I prefer people calling me “favonia” (in any sensible language), thanks.