Homotopy Type Theory: Univalent Foundations of Mathematics. June, 2013.
[see the HoTT blog]
My Homotopy Type Theory Agda library, with lots of computer-checked proofs in homotopy theory.
A Mechanization of the Blakers--Massey Connectivity Theorem in
Homotopy Type Theory. With Favonia, Eric Finster, and Peter LeFanu
A Cubical Approach to Synthetic Homotopy Theory. With Guillaume Brunerie.
Homotopical Patch Theory. With Carlo Angiuli, Ed Morehouse, Robert Harper.
Eilenberg-MacLane Spaces in Homotopy Type Theory. With Eric Finster.
πn(Sn) in Homotopy Type Theory. With Guillaume Brunerie.
Invited paper, CPP 2013.
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
A Functional Programmer's Guide to Homotopy Type Theory.
A 2-categorical framework for substructural modal logics. Talk at
IFIP Working Group 2.8 Meeting. July, 2016.
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.
Cubical Type Theory. Talk at CMU HoTT Seminar. January, 2015.
Type theory podcast episode on HoTT. January, 2015.
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.
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,
A quick introduction to homotopy type theory and its computational interpretation, aimed at mathematicians.
Computing with Univalence. Talk at HDACT'12.
An explanation of the computational interpretation of Homotopy Type Theory, by interpreting types as groupoids.
Denotational Cost Semantics for Functional Languages with Inductive
Datatypes. With Norman Danner and Ramyaa.
Intrinsic Verification of a Regular Expression Matcher.
With Joomy Korkut and Maksim Trifunovski.
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]
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]
Towards Dependent Types over Programmer-Defined Index Domains. With
ConCert meeting talk, March 24, 2005.
This talk describes an early version of the language presented in the technical report above.
A Simple Module System for Twelf. With Rob Simmons and Daniel Lee. Revised December, 2006.
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]