Dan Licata's Publications

Homotopy Type Theory (HoTT)

Books/Dissertation

• Homotopy Type Theory: Univalent Foundations of Mathematics. June, 2013.
  [see the HoTT blog]  
• Dependently Typed Programming with Domain-Specific Logics. February, 2011.
  [pdf]   [defense slides]   [short abstract]

Code

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

Recent Papers

• 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 outlining the project.
  [pdf]
• My articles on the HoTT blog.

Recent Talks

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

Other Papers

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

Other Talks

• Security-Typed Programming within Dependently Typed Programming. With Jamie Morgenstern.
  Dependently Typed Programming, 2010
  [slides pdf]
• The Strange Case of Dr. Admissibility and Mr. Derive.
  Speaking Skills Talk at CMU Student Seminar Series, 2008.
  [slides pdf]
• Mechanizing a Decision Procedure for Coproduct Equality. With Arbob Ahmad and Robert Harper.
  Workshop on Mechanizing Metatheory, 2007
  [slides pdf]
• View Patterns in GHC. With Simon Peyton-Jones.
  AngloHaskell 2007 talk, August 10, 2007.
  [slides pdf]
• 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]

Drafts

• A Simple Module System for Twelf. With Rob Simmons and Daniel Lee. Revised December, 2006.
  [pdf]