📜 Curriculum Vitae of Kuen-Bang Hou (Favonia)

📄 Papers

2025

• 📄 Coslice Colimits in Homotopy Type Theory
  🧑‍🔬 me and Perry Hart
  🌟 CSL 2025 📝 preprint
  🔢 technical report (arXiv)
  🔢 technical report preprint (more updated)

2023

• 📄 An Order-Theoretic Analysis of Universe Polymorphism
  🧑‍🔬 me, Carlo Angiuli and Reed Mullanix
  🌟 POPL 2023 📝 preprint 🐔 Agda 🐫 OCaml
  ⚠️ Errata (fixed in preprint): there was a typo in the AFOSR grant number, and Conor’s slides should have been dated 2012 instead of 2002.

2022

• 📄 Logarithm and Program Testing
  🧑‍🔬 me and Zhuyang Wang
  🌟 POPL 2022 📝 preprint 🔢 proofs 🍛 Haskell 🎬 teaser

2021

• 📄 Syntax and models of Cartesian cubical type theory
  🧑‍🔬 Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, me and Daniel R. Licata
  🌟 MSCS 📝 preprint

2020

• 📄 Cellular Cohomology in Homotopy Type Theory
  🧑‍🔬 Ulrik Buchholtz and me
  🌟 LMCS ⏩ arXiv (direct link)

Older Papers (click to expand)

2018

• 📄 Covering Spaces in Homotopy Type Theory
  🧑‍🔬 me and Robert Harper
  🌟 TYPES 2016 post-proceedings 📝 preprint
  ⚠️ Errata: at the end of section 1, the extended abstract published in 2013 was actually peer-reviewed though it was invited.

• 📄 Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities
  🧑‍🔬 Carlo Angiuli, me and Robert Harper
  🌟 CSL 2018 📝 preprint

• 📄 The RedPRL Proof Assistant (Invited Paper)
  🧑‍🔬 Carlo Angiuli, Evan Cavallo, me, Robert Harper and Jonathan Sterling
  🌟 LFMTP 2018 📝 preprint

• 📄 Cellular Cohomology in Homotopy Type Theory
  🧑‍🔬 Ulrik Buchholtz and me
  🌟 LICS 2018 📝 preprint 📝 arXiv

2017

• 📄 Computational Higher Type Theory III: Univalent Universes and Exact Equality
  🧑‍🔬 Carlo Angiuli, me and Robert Harper
  🌟 updated preprint 📝 arXiv

• 📔 Higher-Dimensional Types in the Mechanization of Homotopy Theory (Ph.D. Thesis)
  🧑‍🏫 advisor: Robert Harper

2016

• 📄 Correctness of Compiling Polymorphism to Dynamic Typing
  🧑‍🔬 me, Nick Benton and Robert Harper
  🌟 JFP 📝 preprint

• 📄 The Seifert–van Kampen Theorem in Homotopy Type Theory
  🧑‍🔬 me and Michael Shulman
  🌟 CSL 2016 📝 preprint

• 📄 A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory
  🧑‍🔬 me, Eric Finster, Daniel R. Licata and Peter LeFanu Lumsdaine
  🌟 LICS 2016 📝 arXiv 📝 preprint

2015

• 📄 A Note on the Uniform Kan Condition in Nominal Cubical Sets
  🧑‍🔬 Robert Harper and me
  📝 arXiv

2013

• 📄 Covering Spaces in Homotopy Type Theory (Extended Abstract)
  🧑‍🔬 me
  🌟 Extended Abstracts Fall 2013 📝 preprint

🗣️ Talks

2024

• 🎙️ asai: a Library for Compiler Diagnostics
  💬 WITS 2024 📅 2024年01月20日
  🎞️ slides

2023

• 🎙️ Building a Proof Assistant
  💬 Midwest PL Summit 2023 📅 2023年10月13日
  🎞️ slides

• 🎙️ Building a Proof Assistant (Invited Talk)
  🏢 Academia Sinica 中央研究院 📅 2023年07月26日
  🎞️ slides (part 1) 🎞️ slides (part 2)

• 🎙️ An Order-Theoretic Analysis of Universe Polymorphism (Invited Talk)
  🏢 Academia Sinica 中央研究院 📅 2023年07月19日

• 🎙️ Logarithm and Program Testing (Invited Talk)
  💬 Functional Thursday 📅 2023年07月13日
  🎞️ slides (in Mandarin)

• 🎙️ Logarithm and Program Testing (Invited Talk)
  🏢 Academia Sinica 中央研究院 📅 2023年07月13日

• 🎙️ An Order-Theoretic Analysis of Universe Polymorphism
  💬 POPL 2023 📅 2023年1月19日
  🎬 YouTube 🎞️ slides

2022

• 🎙️ An Order-Theoretic Analysis of Universe Polymorphism
  💬 Workshop on Dependent Type Theory 📅 2022年12月14日

• 🎙️ Building a Proof Assistant
  💬 PurPL seminar 📅 2022年09月30日
  🎞️ slides

• 🎙️ Cartesian cubical type theory
  🏫 HoTTEST Summer School 📅 2022年08月29日
  🎬 YouTube 🎞️ slides

• 🎙️ A Domain-Specific Language for Name Modifiers
  💬 TYPES 📅 2022/06
  🎬 YouTube 🎞️ slides 📝 abstract preprint

• 🎙️ Logarithm and Program Testing
  💬 PurPL seminar 📅 2022年03月25日
  🎞️ slides

2021

• 🎙️ Program Testing with Polymorphic Types
  💬 UMN CS&E Colloquia 📅 2021年12月06日
  🎞️ slides

2020

• 🎙️ Nullable Compositions (invited)
  💬 Univalent Mathematics: Theory and Implementation (ICMS 2020 session) 📅 2020年07月15日
  🎬 YouTube 🎞️ slides

Older Talks (click to expand)

2019

• 🎙️ Nullable Compositions
  💬 Midwest Homotopy Type Theory Seminar 📅 2019年10月19日

• 🎙️ Rise of Higher-Dimensional Types (SCS Distinguished Doctoral Dissertation Award Lecture)
  🏫 Carnegie Mellon University 📅 2019年08月30日
  🎞️ slides

• 🎙️ Introduction to Cubical Type Theory (Invited Talk)
  🏫 Logic Mentoring Workshop 📅 2019年06月22日
  🎞️ slides

• 🎙️ Logarithm and Program Testing
  💬 UMN Programming Language Seminar 📅 2019年06月05日

• 🎙️ Logarithm and Program Testing
  👥 IFIP Working Group 2.8 📅 2019年05月20日

2018

• 🎙️ Normalization in Cubical Type Theory
  🏫 University of Gothenburg 📅 2018年10月29日

• 🎙️ Normalization in Cubical Type Theory
  💬 Stockholm Logic Seminar 📅 2018年10月24日

• 🎙️ Towards Efficient Cubical Type Theory
  💬 HoTTEST 📅 2018年10月11日
  🎬 YouTube 🎞️ slides

• 🎙️ redtt: cartesian cubical type theory
  🏢 Center for Advanced Study 📅 2018年08月28日
  🎞️ slides

• 🎙️ 多型:無知就是力量 Polymorphism: Ignorance is Power (Invited Talk)
  💬 Functional Thursday 📅 2018年08月02日
  🎬 YouTube 🎞️ slides (in Mandarin)
  ⚠️ Errata: the theorem for filter is wrong. bool is not general enough.

• 🎙️ Cartesian Cubical Computational Type Theory (Invited Talk)
  🏢 Academia Sinica 中央研究院 📅 2018年07月26日
  🎞️ slides

• 🎙️ Cellular Cohomology in Homotopy Type Theory
  💬 LICS 📅 2018年07月09日
  🎞️ slides

• 🎙️ Cubical Computational Type Theory
  💬 HoTT/UF 📅 2018年07月08日
  🎞️ slides

• 🎙️ Cubical Computational Type Theory and RedPRL (Invited Talk)
  💬 LFMTP 📅 2018年07月07日
  🎞️ slides

• 🎙️ Cartesian Cubical Computational Type Theory
  💬 Workshop: Types, Homotopy Type Theory, and Verification 📅 2018年06月05日
  🎬 YouTube 🎞️ slides

• 🎙️ Cubical Computational Type Theory and RedPRL
  🏫 Princeton University 📅 2018年04月17日

• 🎙️ Multiverses in Computational Higher Type Theory
  💬 MURI grant meeting 📅 2017年03月23日
  📝 notes

• 🎙️ Expressive Types
  🏫 University of Minnesota 📅 2018年03月02日

• 🎙️ Cubical Computational Type Theory and RedPRL
  👥 Penn PLClub 📅 2018年02月23日
  🎞️ slides

• 🎙️ Cubical Computational Type Theory
  💬 Cornell PLDG 📅 2018年02月07日
  🎞️ slides

2017

• 🎙️ Mechanized Reasoning in Mathematics
  🏢 Institute for Advanced Study 📅 2017年09月29日
  🎞️ slides 🎬 video

• 🎙️ Homotopy Type Theory in Agda
  💬 Big Proof 📅 2017年07月07日
  🎬 video 🎞️ slides

• 🎙️ Computational Higher-Dimensional Type Theory
  💬 Big Proof 📅 2017年07月04日
  🎬 video 🎞️ slides

• 🎙️ Compiling Polymorphism to Dynamic Typing
  💬 PLunch 📅 2017年04月07日
  🎞️ slides

• 🎙️ Axiomatic and cellular cohomology theory
  💬 MURI grant meeting 📅 2017年03月25日
  🎞️ slides

2016

• 🎙️ The Seifert-van Kampen Theorem in Homotopy Type Theory 💬 CSL 📅 2016年08月30日
  🎞️ slides

• 🎙️ A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory
  💬 LICS 📅 2016年07月07日
  🎞️ slides (the title was rendered broken)

• 🎙️ The Seifert-van Kampen Theorem in Homotopy Type Theory
  💬 Workshop on Homotopy Type Theory and Univalent Foundations of Mathematics 📅 2016年05月16日
  🎬 video 🎞️ slides

2014

• 🎙️ Covering Spaces in Homotopy Type Theory
  💬 TYPES 📅 2014年05月13日
  🎞️ slides 📝 abstract preprint

2013

• 🎙️ Covering Spaces in Homotopy Type Theory
  💬 Conference on Type Theory, Homotopy Theory and Univalent Foundations 📅 2013年09月27日
  🎞️ slides 📝 abstract 📝 abstract preprint

2012

• 🎙️ 給電腦科學家的邏輯系統 (Logic Systems for Computer Scientists)
  💬 FLOLAC 📅 2012年08月30日
  🎞️ slides (in Mandarin)

📦 Artifacts

• 🔴 The red* family of proof assistants
  The website for cooltt, redtt, RedPRL, and many other components

• 🔥 HoTT-Agda: development of homotopy type theory in Agda

💁 Services

Short-Term

• 👥 MSFP 2026 🤩 Organizer
• 👥 ICFP 2025 Student Research Competition (SRC) 🤩 Organizer
• 👥 ICFP 2024 Student Research Competition (SRC) 🤩 Organizer
• 👥 School on Univalent Mathematics 2024 🤩 Organizer
• 👥 MSFP 2024 🤩 Organizer
• 💬 POPL 2024 🥸 PC
• 💬 CPP 2024 🥸 PC
• 👥 PLMW@POPL 2023 🤩 Organizer
• 💬 MFPS 2022 🥸 PC
• 💬 SPIN 2022 🥸 PC
• 💬 POPL 2022 🤗 Panelist
• 📄 NSF (Unspecified) Review Panel 2022 😶‍🌫️ Panelist
• 💬 HoTT/UF 2021 🥸 PC
• 💬 ICFP 2021 🥸 PC
• 👥 PLMW@POPL 2021 🤗 Panelist + 🤗 Mentor
• 💬 ICFP 2017 🥸 AEC Member
• 👥 School and Workshop on Univalent Mathematics 🤗 Mentor
• 📄 NSF (Unspecified) Review Panel 2020 😶‍🌫️ Panelist
• 👥 Logical Mentoring Workshop 2017 🤗 Panelist

Longer-Term

• 👥 SIGPLAN-M 🤗 Mentor

🏅 Awards

• ✍️ Distinguished Reviewer Award 💬 ICFP 📅 2021
• 📔 School of Computer Science Distinguished Dissertation Award 🏫 Carnegie Mellon University 📅 2016/2017

🧑‍🏫 Teaching

• 🏫 UMN CSCI 5106 Programming Languages 📅 2024 Fall
• 🏫 UMN CSCI 5980/8980 Programming Language Theory 📅 2024 Spring
• 🏫 UMN CSCI 8980 Introduction to Dependent Type Theory 📅 2023 Fall
• 🏫 UMN CSCI 2041 Advanced Programming Principles 📅 2023 Spring
• 🏫 UMN CSCI 8980 Programming Language Foundations in Agda 📅 2021 Fall
• 🏫 UMN CSCI 5106 Programming Languages 📅 2021 Fall
• 🏫 UMN CSCI 2041 Advanced Programming Principles 📅 2021 Spring
• 🏫 UMN CSCI 5106 Programming Languages 📅 2020 Fall
• 🏫 UMN CSCI 8980 Higher Dimensional Type Theory 📅 2020 Spring
• 🏫 UMN CSCI 2041 Advanced Programming Principles 📅 2019 Fall

📜 Work History

• 🏫 University of Minnesota 📍 Minneapolis, MN, USA
  🪪 Assistant Professor 📅 2018–

🎓 Education

• 🏢 Institute for Advanced Study 📍 Princeton, NJ, USA
  🪪 Postdoctoral Member 📅 2017–2018

• 🏫 Carnegie Mellon University 📍 Pittsburgh, PA, USA
  🪪 Postdoctoral Faculty 📅 2017

• 🏫 Carnegie Mellon University 📍 Pittsburgh, USA
  🎓 Ph.D., Computer Science 📅 2017
  📔 Thesis: Higher-Dimensional Types in the Mechanization of Homotopy Theory
  🧑‍🏫 Advisor: Robert Harper

• 🏢 Academia Sinica 📍 Taiwan
  🪪 Research Assistant 📅 2009–2010

• 🏫 National Taiwan University 📍 Taiwan
  🎓 B.S., Computer Science and Information Engineering 📅 2008

• 🏫 Massachusetts Institute of Technology 📍 Massachusetts, USA
  🌼 Special Student, Electrical Engineering and Computer Science 📅 2006–2007

---

Homepage

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