Homotopy Type Theory


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.


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.

Homotopical Patch Theory. With Carlo Angiuli, Ed Morehouse, Robert Harper.
ICFP, 2014.

Eilenberg-MacLane Spaces in Homotopy Type Theory. With Eric Finster.
LICS, 2014

πn(Sn) in Homotopy Type Theory. With Guillaume Brunerie.
Invited paper, CPP 2013.

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

Foundations and Applications of Higher-Dimensional Directed Type Theory. With Robert Harper.

Research statement. April 2013


Cubical Type Theory. Talk at AFOSR MURI Team Meeting. March, 2015.

Cubical Type Theory. Talk at CMU HoTT Seminar. January, 2015.

Type theory podcast episode on HoTT. January, 2015.

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.

Cubical Type Theory. Talk at IFIP WG 2.8. August, 2014.

What is Homotopy Type Theory? Invited talk at Coq Workshop, 2014.

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.

Lectures on Homotopy Type Theory. Mathematical Structures of Computation, Lyon. January, 2014.

Programming and Proving with Higher Inductive Types. Invited Talk at CPP 2013.

Mathematical and Computational Applications of Homotopy Type Theory.
Colloquium at University of Iowa. November, 2013.

Git as a HIT. Talk at IFIP WG 2.8. October, 2013.

Lectures on Agda at OPLSS'13. Lectures 4 and 5 discuss programming in HoTT.

Computer-Checked Proofs in the Logic of Homotopy Theory.
Invited Talk at the Association for Symbolic Logic North American Meeting. May, 2013.

Programming and Proving in Homotopy Type Theory.
Colloquium at Wesleyan, Princeton, and Cornell. Spring, 2013.

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.

A Computer-Checked Proof that the Fundamental Group of the Circle is the Integers. Talk at IAS Members Seminar, November, 2012.
Aimed at mathematicians without prior knowledge of type theory.

Programming in Homotopy Type Theory. Talk at IFIP Wroking Group 2.8 meeting, November, 2012.
Applications of HoTT to programming, including code reuse and specs for abstract types.

Towards a Computational Interpretation of HoTT. Chalk talk at IAS. October, 2012.
Some technical details on 2D type theory; unfortunately, the punch-line was pre-empted by a fire alarm.

Computing with Univalence. Post-doctoral member talk at IAS. September, 2012.
A quick introduction to homotopy type theory and its computational interpretation, aimed at mathematicians.
[video] [slides]  

Computing with Univalence. Talk at HDACT'12.
An explanation of the computational interpretation of Homotopy Type Theory, by interpreting types as groupoids.

Cost Analysis

Denotational Cost Semantics for Functional Languages with Inductive Datatypes. With Norman Danner and Ramyaa.
ICFP, 2015.

Dependent Types

Intrinsic Verification of a Regular Expression Matcher. With Joomy Korkut and Maksim Trifunovski.
Submitted, 2016.

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.

Other Topics


View Patterns in GHC. With Simon Peyton-Jones.
Talk at AngloHaskell 2007 August 10, 2007.
[slides pdf]

Software Engineering

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]

Programming Contest

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]