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