Homotopy Type Theory: Univalent Foundations of Mathematics. June, 2013.
[see the HoTT blog]
PhD Thesis: Dependently Typed Programming with Domain-Specific Logics. Advised by Bob Harper.
February, 2011.
[pdf] [defense slides]
[short abstract]
My Homotopy Type Theory Agda library, with lots of computer-checked proofs in homotopy theory.
My articles on the HoTT blog.
A Constructive Model of Directed Univalence in Bicubical Sets.
With Matthew Z. Weaver.
LICS, 2020
[pdf]
Gradual Type Theory.
With Max S. New and Amal Ahmed.
POPL, 2019
[pdf]
[long version arxiv]
Call-by-name Gradual Type Theory.
With Max S. New.
FSCD, 2018; LMCS, 2020.
[conference pdf]
[journal version arxiv]
Internal Universes in Models of Homotopy Type Theory.
With Ian Orton, Andrew M. Pitts, and Bas Spitters.
FSCD, 2018
[arxiv]
Cartesian Cubical Type Theory.
With Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Kuen-Bang Hou
(Favonia), and Robert Harper.
[draft]
[formalization]
A Fibrational Framework for Substructural and Modal Logics. With
Mike Shulman and Mitchell Riley.
FSCD, 2017.
[short pdf]
[extended pdf]
[slides]
A Mechanization of the Blakers--Massey Connectivity Theorem in
Homotopy Type Theory. With Favonia, Eric Finster, and Peter LeFanu
Lumsdaine.
LICS, 2016.
[pdf]
Adjoint logic with a 2-category of modes. With Mike Shulman.
LFCS, 2016.
[extended pdf],
[slides]
A Cubical Approach to Synthetic Homotopy Theory. With Guillaume Brunerie.
LICS, 2015.
[pdf]
Homotopical Patch Theory. With Carlo Angiuli, Ed Morehouse, Robert Harper.
ICFP, 2014. JFP, 2016.
[conf pdf],
[journal pdf]
Eilenberg-MacLane Spaces in Homotopy Type Theory. With Eric Finster.
LICS, 2014
[pdf]
πn(Sn) in Homotopy Type Theory. With Guillaume Brunerie.
Invited paper, CPP 2013.
[pdf]
Calculating the Fundamental Group of the Circle in Homotopy Type Theory. With Michael Shulman.
LICS 2013.
[pdf]
[Agda code]
Canonicity for 2-Dimensional Type Theory. With Robert Harper.
POPL 2012.
[final pdf]
[draft (with appendix) pdf]
[slides]
[video (ACM)]
2-Dimensional Directed Dependent Type Theory. With Robert Harper.
MFPS 2011.
See also Chapters 7 and 8 of my thesis.
[pdf] [slides]
Homotopy Type Theory: Unified Foundations of Mathematics and Computation
[pdf]
Foundations and Applications of Higher-Dimensional Directed Type Theory. With Robert Harper.
[pdf]
Research statement. April 2013
[pdf]
A Fibrational Framework for Substructural and Modal Dependent Type Theories.
HoTT Electronic Seminar Series, 2019. HoTT 2019.
[video]
[slides]
Univalence from a Computer Science Point-of-View.
Voevodsky Memorial Conference, 2018.
[video]
[slides]
[cubicaltt code]
Synthetic Mathematics in Modal Dependent Type Theories.
6-talk tutorial joint with Felix Wellen.
Hausdorff Institute Workshop on Types, Homotopy Type theory, and
Verification, 2018.
[videos here]
[slides for my talks]
Bicubical Directed Type Theory. AFOSR MURI Team Meeting, March, 2018.
Dependent Modal Type Theory, Syntactically. AFOSR MURI Team Meeting, March, 2018.
Small Proofs. Big Proof Program, Workshop on Computer-aided Mathematical
Proof, 2017.
[video]
[slides]
A Fibrational Framework for Substructural and Modal Logics. Talk at AFOSR MURI Team Meeting, March, 2017.
A Functional Programmer's Guide to Homotopy Type Theory. Invited talk at ICFP 2016.
[video]
[slides]
A 2-categorical framework for substructural modal logics. Talk at
IFIP Working Group 2.8 Meeting, July, 2016.
[slides]
Cubical Type Theory.
Workshop on Homotopy Type Theory and Univalent
Foundations of Mathematics, The Fields Institute. May, 2016.
[video 1],
[video 2]
Adjoint logic with a 2-category of modes. Talk at AFOSR MURI Team Meeting. March, 2016.
Cubical Type Theory. Talk at AFOSR MURI Team Meeting. March, 2015.
[slides]
Cubical Type Theory. Talk at CMU HoTT Seminar. January, 2015.
Type theory podcast episode on HoTT. January, 2015.
[link]
A Cubical Infinite-Dimensional Type Theory.
Talk at Oxford Homotopy Type Theory Workshop. November, 2014.
[slides],
[video]
Functional programs that prove theorems about spaces. Talk at Brown University. October, 2014.
[slides]
Cubical Type Theory. Talk at IFIP WG 2.8. August, 2014.
[slides]
What is Homotopy Type Theory? Invited talk at Coq Workshop, 2014.
[slides]
Lectures on Homotopy Type Theory. Microsoft Research, Redmond. May, 2014.
Eilenberg-MacLane Spaces in Homotopy Type Theory.
Invited talk at
Workshop on Formalization of Mathematics in Proof Assistants,
Thematic trimester on
Semantics of Proofs and Certified Mathematics, Institute Henri Poincaré.
May, 2014. Also given at LICS, 2014.
[slides]
Lectures on Homotopy Type Theory. Mathematical Structures of Computation, Lyon. January, 2014.
Programming and Proving with Higher Inductive Types. Invited talk at CPP 2013.
[slides]
Mathematical and Computational Applications of Homotopy Type Theory.
Colloquium at University of Iowa. November, 2013.
[slides]
Git as a HIT. Talk at IFIP WG 2.8. October, 2013.
[slides]
Lectures on Agda at OPLSS'13. Lectures 4 and 5 discuss programming in HoTT.
[videos]
Computer-Checked Proofs in the Logic of Homotopy Theory.
Invited talk at the Association for Symbolic Logic North American Meeting. May, 2013.
[slides]
Programming and Proving in Homotopy Type Theory.
Colloquium at Wesleyan, Princeton, and Cornell. Spring, 2013.
[slides]
Homotopy Theory in Type Theory: Summary of Results. With Guillaume
Brunerie and Peter Lumsdaine.
Talk at IAS. April, 2013.
[video]
[slides]
Eilenberg-Mac Lane Spaces in HoTT. Chalk talk at IAS. March, 2013.
[video]
A Computer-Checked Proof that the Fundamental Group of the Circle is the Integers.
Talk at IAS Members Seminar, November, 2012.
[video]
Programming in Homotopy Type Theory. Talk at IFIP Wroking Group 2.8
meeting, November, 2012.
[slides]
Towards a Computational Interpretation of HoTT. Chalk talk at IAS. October, 2012.
[video]
Computing with Univalence. Post-doctoral member talk at IAS. September,
2012.
[video]
[slides]
Computing with Univalence. Talk at HDACT'12.
[slides]
Denotational Recurrence Extraction for Amortized Analysis.
With Joseph W. Cutler and Norman Danner.
ICFP, 2020
[pdf]
[arxiv]
Recurrence Extraction for Functional Programs through
Call-by-Push-Value.
With Alex Kavvos, Ed Morehouse, and Norman Danner.
POPL, 2020
[pdf]
[extended pdf]
Denotational Cost Semantics for Functional Languages with Inductive
Datatypes. With Norman Danner and Ramyaa.
ICFP, 2015.
[pdf]
A Taste of Dependent Types.
PLMW at ICFP 2016.
[video]
[Agda code]
[Agda library]
(download both to same directory)
Intrinsic Verification of a Regular Expression Matcher.
With Joomy Korkut and Maksim Trifunovski.
2016.
[pdf]
Security-Typed Programming within Dependently-Typed Programming. With Jamie Morgenstern.
In International Conference on Functional Programming, 2010.
[abstract]
[bibtex]
[pdf]
[Agda code]
[slides]
[talk video]
Security-Typed Programming within Dependently Typed Programming. With Jamie Morgenstern.
Talk at Dependently Typed
Programming, 2010
[slides pdf]
A Monadic Formalization of ML5. With Robert Harper.
In Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, EPTCS 34, 2010.
[arXiv]
[abstract]
[bibtex]
[pdf]
[Agda code]
A Universe of Binding and Computation. With Robert Harper.
In International Conference on Functional Programming, 2009.
[abstract]
[bibtex]
[pdf]
[Agda code]
[slides pdf]
[talk video]
Positively Dependent Types. With Robert Harper.
In ACM SIGPLAN Workshop on Programming Languages Meets Program Verification, January 2009.
[abstract]
[bibtex]
[pdf]
[Agda code]
[slides pdf]
Focusing on Binding and Computation. With Noam Zeilberger and Robert Harper.
In IEEE Symposium on Logic in Computer Science, June 2008.
Long version available as Technical Report CMU-CS-08-101, February, 2008.
[abstract]
[bibtex]
[conference pdf]
[TR pdf]
[Agda code]
[Coq code]
[slides pdf]
Mechanizing Metatheory in a Logical Framework. With Robert Harper.
Journal of Functional Programming, 17(4-5), July 2007.
A technical introduction to LF and Twelf. You can learn more about LF and Twelf at the Twelf Wiki.
[abstract]
[bibtex]
[pdf]
[Twelf code]
A Formulation of Dependent ML with Explicit Equality Proofs. With Robert Harper.
Technical Report CMU-CS-05-178, December, 2005.
[abstract]
[bibtex]
[pdf]
[Twelf code]
Towards Dependent Types over Programmer-Defined Index Domains. With
Robert Harper.
ConCert meeting talk,
March 24, 2005.
This talk describes an early version of the language presented in the
technical report above.
[slides pdf]
The Strange Case of Dr. Admissibility and Mr. Derive.
Speaking Skills Talk at Talk at CMU Student Seminar
Series, 2008.
[slides pdf]
Mechanizing a Decision Procedure for Coproduct Equality. With Arbob
Ahmad and Robert Harper.
Talk at Workshop on
Mechanizing Metatheory, 2007
[slides pdf]
A Simple Module System for Twelf. With Rob Simmons and Daniel Lee. Revised December, 2006.
[pdf]
View Patterns in GHC. With Simon Peyton-Jones.
Talk at AngloHaskell 2007
August 10, 2007.
[slides pdf]
Verifying Interactive Web Programs. With Shriram Krishnamurthi.
In IEEE International Symposium on Automated Software
Engineering, 2004.
Long version available as Brown University Undergraduate Honors Thesis, 2004.
[abstract]
[bibtex]
[pdf]
[long pdf]
[slides ppt]
The Feature Signatures of Evolving Programs. With Christopher Harris and Shriram Krishnamurthi.
In IEEE International Symposium on Automated Software Engineering, 2003.
A.k.a. Brown CS TR CS-03-12.
[abstract]
[bibtex]
[tech. report pdf]
The Cult of the Bound Variable: The 9th Annual ICFP Programming Contest.
With Tom Murphy VII, Daniel Spoonhower, Chris Casinghino, Karl Crary, and Robert Harper.
Working title: A Dependently-Typed Domain-Specific Language for Computational Archaeolinguistics.
Grol Blirtri's name was
removed from this paper when he was found not to exist.
Technical Report CMU-CS-06-163, October, 2006.
[abstract]
[bibtex]
[pdf]
[contest Web page]