📜 Curriculum Vitae of Kuen-Bang Hou (Favonia)

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

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)