- Homepage: favonia.org
- Email: FAVONIA at GMAIL

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

Covering Spaces in Homotopy Type Theory

*with Robert Harper*.

[draft] (submitted to the TYPES 2016 post-proceedings)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, Dan 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

- 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

Minimalism with GitHub-like CSS (licensed under MIT).