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

Logarithm and Program Testing

Note: the current draft contains a serious technical error that will be fixed. The current theorem is false but can be rescued with a mild modification.Syntax and Models of Cartesian Cubical Type Theory

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

[preprint]

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]

- 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/05

Note: the conjecture turns out to be false. Please check the upcoming paper(s).Logarithm and Program Testing

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

Note: the conjecture turns out to be false. Please check the upcoming paper(s).

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

- Instructor of UMN CSCI 5106: Programming Languages, 2020 Fall
- Instructor of UMN CSCI 8980: Higher Dimensional Type Theory, 2020 Spring
- Instructor of UMN CSCI 2041: Advanced Programming Principles, 2019 Fall
- Teaching Assistant of CMU 15-814: Type Systems for Programming Languages, Fall 2012
- Teaching Assistant of CMU 15-210: Parallel and Sequential Data Structures and Algorithms, Fall 2015

- Member of ICFP 2017 Artifact Evaluation Committee
- Mentor of School and Workshop on Univalent Mathematics

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