๐ 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
๐ 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
๐ 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
๐๏ธ 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
๐๏ธ 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
๐๏ธ 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
๐๏ธ 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
๐๏ธ 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
๐๏ธ 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
๐ด The red* family of proof assistants
The website for cooltt, redtt, RedPRL, and many other components
๐ข 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
This page was made with GitHub-like CSS (licensed under MIT and modified by me).