Carnegie Mellon University, Pittsburgh, USA

Ph.D., Computer Science, 2017

Thesis: Higher-Dimensional Types in the Mechanization of Homotopy TheoryNational Taiwan University, Taiwan

B.S., Computer Science and Information Engineering, 2008Massachusetts Institute of Technology, Massachusetts, USA

Special Student, Electrical Engineering and Computer Science, 2006–2007

University of Minnesota, Minneapolis, MN, USA

Assistant Professor, 2018–Institute for Advanced Study, Princeton, NJ, USA

Postdoctoral Member, 2017–2018Carnegie Mellon University, Pittsburgh, PA, USA

Postdoctoral Faculty, 2017Academia Sinica, Taiwan

Research Assistant, 2009–2010

Syntax and models of Cartesian cubical type theory

*with Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper and Daniel R. Licata*

[MSCS] [preprint]Logarithm and Program Testing

*with Zhuyang Wang*

[POPL 2022] [preprint] [proofs] [teaser]

- Cellular Cohomology in Homotopy Type Theory

*with Ulrik Buchholtz*

[LMCS] [arXiv direct link]

Covering Spaces in Homotopy Type Theory

*with Robert Harper*

[TYPES 2016 post-proceedings] [preprint]

Errata: at the end of section 1, the extended abstract published in 2013 was actually peer-reviewed but was invited.Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities

*with Carlo Angiuli and Robert Harper*

[CSL 2018] [preprint]The RedPRL Proof Assistant (Invited Paper)

*with Carlo Angiuli, Evan Cavallo, Robert Harper and Jonathan Sterling*

[LFMTP 2018] [preprint]Cellular Cohomology in Homotopy Type Theory

*with Ulrik Buchholtz*

[LICS 2018] [preprint] [arXiv]

Computational Higher Type Theory III: Univalent Universes and Exact Equality

*with Carlo Angiuli and Robert Harper*

[updated preprint] [arXiv]Higher-Dimensional Types in the Mechanization of Homotopy Theory (Ph.D. Thesis)

Correctness of Compiling Polymorphism to Dynamic Typing

*with Nick Benton and Robert Harper*.

[JFP] [preprint]The Seifert–van Kampen Theorem in Homotopy Type Theory

*with Michael Shulman*.

[CSL 2016] [preprint]A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory

*with Eric Finster, Daniel R. Licata and Peter LeFanu Lumsdaine*.

[LICS 2016] [arXiv] [preprint]

- A Note on the Uniform Kan Condition in Nominal Cubical Sets

*with Robert Harper*.

[arXiv]

- Covering Spaces in Homotopy Type Theory (Extended Abstract)

[Extended Abstracts Fall 2013] [preprint]

- Logarithm and Program Testing
*in*the PurPL seminar 2022/03/25

[slides]

- Program Testing with Polymorphic Types
*in*the Computer Science & Engineering Colloquia 2021/12/06

[slides]

- Nullable Compositions
*in*the Univalent Mathematics: Theory and Implementation session of ICMS 2020 (invited) 2020/07/15

[video (YouTube copy)] [slides]

Nullable Compositions

*at*Midwest Homotopy Type Theory Seminar 2019/10/19Rise of Higher-Dimensional Types (SCS Distinguished Doctoral Dissertation Award Lecture)

*at*Carnegie Mellon University 2019/08/30

[slides]Introduction to Cubical Type Theory (Invited Talk)

*at*Logic Mentoring Workshop 2019/06/22

[slides]Logarithm and Program Testing

*at*Programming Language Seminar 2019/06/05Logarithm and Program Testing

*at*IFIP Working Group 2.8 2019/05/20

Normalization in Cubical Type Theory

*at*University of Gothenburg 2018/10/29Normalization in Cubical Type Theory

*in*Stockholm Logic Seminar*at*Stockholm University 2018/10/24Towards Efficient Cubical Type Theory

*at*Homotopy Type Theory Electronic Seminar Talks (HoTTEST) 2018/10/11

[slides] [video]redtt: cartesian cubical type theory

*at*Center for Advanced Study (Senter for grunnforskning) 2018/08/28

[slides]多型：無知就是力量 Polymorphism: Ignorance is Power (Invited Talk)

*at*Functional Thursday 2018/08/02

[slides (in Mandarin)] [video]

Errata: the theorem for filter is wrong. bool is not general enough.Cartesian Cubical Computational Type Theory (Invited Talk)

*in*Academia Sinica 中央研究院 2018/07/26

[slides]Cellular Cohomology in Homotopy Type Theory

*at*LICS 2018/07/09

[slides]Cubical Computational Type Theory

*at*HoTT/UF 2018/07/08

[slides]Cubical Computational Type Theory and RedPRL (Invited Talk)

*at*LFMTP 2018/07/07

[slides]Cartesian Cubical Computational Type Theory

*at*Workshop: Types, Homotopy Type Theory, and Verification 2018/06/05

[slides] [video]Cubical Computational Type Theory and RedPRL

*at*Princeton University 2018/04/17Multiverses in Computational Higher Type Theory

*at*MURI grant meeting 2017/03/23

[notes]Expressive Types

*at*University of Minnesota 2018/03/02

[link]Cubical Computational Type Theory and RedPRL

*at*Penn PLClub 2018/02/23

[slides]Cubical Computational Type Theory

*at*Cornell PLDG 2018/02/07

[slides]

Mechanized Reasoning in Mathematics

*at*Institute for Advanced Study 2017/09/29

[slides] [video]Homotopy Type Theory in Agda

*at*Big Proof 2017/07/07

[slides] [video]Computational Higher-Dimensional Type Theory

*at*Big Proof 2017/07/04

[slides] [video]Compiling Polymorphism to Dynamic Typing

*at*PLunch 2017/04/07

[slides]Axiomatic and cellular cohomology theory

*at*MURI grant meeting 2017/03/25

[slides]

The Seifert-van Kampen Theorem in Homotopy Type Theory

*at*CSL 2016/08/30

[slides]A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory

*at*LICS 2016/07/07

[slides (the title was rendered broken)]The Seifert-van Kampen Theorem in Homotopy Type Theory

*at*Workshop on Homotopy Type Theory and Univalent Foundations of Mathematics 2016/05/16

[slides] [recording]

- Covering Spaces in Homotopy Type Theory
*at*TYPES 2014/05/13

[slides] [abstract preprint]

- Covering Spaces in Homotopy Type Theory
*at*Conference on Type Theory, Homotopy Theory and Univalent Foundations 2013/09/27

[slides] [abstract] [abstract preprint]

HoTT-Agda: development of homotopy type theory in Agda

Maintainer and DeveloperRedPRL: a proof assistant for computational high-dimensional type theory

Developerredtt: an experimental implementation addressing some issues in RedPRL

Developer

- 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

- Member of SPIN 2022 Program Committee
- Member of ICFP 2021 Program Committee
- Mentor of POPL 2021 PLMW
- Member of ICFP 2017 Artifact Evaluation Committee
- Mentor of School and Workshop on Univalent Mathematics

- Distinguished Reviewer Award, ICFP, 2021
- School of Computer Science Distinguished Dissertation Award, Carnegie Mellon University, 2016/2017

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