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 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.

[pdf]

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

LICS, 2014

[pdf]

π_{n}(S^{n}) 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 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.

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]

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

ICFP, 2015.

[pdf]

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

Submitted, 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 9^{th} 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]