Research on Homotopy Type Theory

For my work on other topics, see below.

Books

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]

Code

My Homotopy Type Theory Agda library, with lots of computer-checked proofs in homotopy theory.

Blog

My articles on the HoTT blog.

Papers

Eilenberg-MacLane Spaces in Homotopy Type Theory. With Eric Finster.
[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]  

Foundations and Applications of Higher-Dimensional Directed Type Theory. With Robert Harper.
Grant proposal.
[pdf]

Research statement. April 2013
[pdf]

Talks

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]

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.
Aimed at mathematicians without prior knowledge of type theory.
[video]

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.
[slides]  

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.
[video]

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.
[slides]  

Press about HoTT

The Institute Letter, Summer 2013

Wired, June 2013

Research on Other Topics

Dependent Types

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]  

Haskell

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]