Drafts

• Dependently Typed Programming With Domain-Specific Logics. With Robert Harper. Revised July, 2008.
  [pdf]  
• 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]  

Papers

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

Talks

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

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]