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

Institute for Advanced Study, Princeton, USA

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

Postdoctoral Faculty, 2017Academia Sinica, Taiwan

Research Assistant, 2009–2010

Cartesian Cubical Type Theory

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

[draft]Covering Spaces in Homotopy Type Theory

*with Robert Harper*.

[draft] (submitted to the TYPES 2016 post-proceedings)

Computational Higher Type Theory III: Univalent Universes and Exact Equality

*with Carlo Angiuli and Robert Harper*

[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] [draft]The Seifert–van Kampen Theorem in Homotopy Type Theory

*with Michael Shulman*.

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

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

[LICS 2016 proceeding] [arXiv] [draft]

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

*with Robert Harper*.

[arXiv]

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

[slides]

The Seifert-van Kampen Theorem in Homotopy Type Theory

*at*CSL 2016

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

*at*LICS 2016

[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)

[slides] [recording]

- Covering Spaces in Homotopy Type Theory
*at*TYPES 2014

[slides] [abstract draft]

- Covering Spaces in Homotopy Type Theory
*at*Conference on Type Theory, Homotopy Theory and Univalent Foundations (2013)

[slides] [abstract] [abstract draft]

- 給電腦科學家的邏輯系統 (Logic Systems for Computer Scientists)
*at*FLOLAC 2012

[slides]

HoTT-Agda: development of homotopy type theory in Agda

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

Developer

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

- 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

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