Dan Licata's Publications

New!

• Canonicity for 2-Dimensional Type Theory. With Robert Harper.
  Draft as of July, 2011. To appear in POPL 2012.
  [pdf]
• 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]

Dissertation

• Dependently Typed Programming with Domain-Specific Logics. February, 2011.
  [pdf]   [defense slides]  

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]  
• Dependently Typed Programming With Domain-Specific Logics.
  Short version with Robert Harper, revised July, 2008. Thesis proposal revised October, 2008.
  [short pdf]   [thesis proposal pdf]   [thesis proposal 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

• An Extensible Theory of Indexed Types. With Robert Harper. Revised July, 2007.
  [pdf]  
• A Simple Module System for Twelf. With Rob Simmons and Daniel Lee. Revised December, 2006.
  [pdf]  

Code

• Agda proof of cut and identity for the negative half of polarized intuitionistic logic
  (a.k.a. hereditary substitution for STLC)
  [tar gz]   [main file agda]
• Two Agda proofs of normalization for Godel's T
  [tar gz]