The PROSPERO Project

PROpositions, SPEcifications, and ReasOning

The Prospero Project seeks to extend the type systems of languages like ML and Haskell to support the verification of a richer collection of program properties. A key ingredient in our approach is making it easy for programmers to define domain-specific logics for reasoning about their software. We are investigating new tools for representing and computing with logics in a programming language, as well as applications of this technology to software verification. The Prospero Project is a collaborative investigation with the Ynot Project at Harvard.

Researchers

At Carnegie Mellon University:

• Robert Harper (co-principal-investigator)
• Frank Pfenning (co-principal-investigator)
• Dan Licata (graduate student)
• Arbob Ahmad (graduate student)

Elsewhere:

• Greg Morrisett, Harvard (co-principal-investigator) and the members of the Ynot Project
• Noam Zeilberger, Paris 7

Drafts, Publications, and Talks

• A Universe of Binding and Computation.
  Daniel R. Licata and Robert Harper.
  To appear at the International Conference on Functional Programming, 2009.
  [pdf, March 2009]   [Agda code]  
• Positively Dependent Types.
  Daniel R. Licata and Robert Harper.
  In Workshop on Programming Languages Meets Program Verification, January 2009.
  [abstract]   [bibtex]   [pdf]   [Agda code]   [slides pdf]  
• Dependently Typed Programming With Domain-Specific Logics.
  Daniel R. Licata
  Thesis proposal, 2008.
  [thesis proposal pdf]   [thesis proposal slides pdf]  
• Focusing on Binding and Computation.
  Daniel R. Licata and 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.
  Daniel R. Licata and Robert Harper.
  Journal of Functional Programming, 17(4-5), July 2007.
  [abstract]   [bibtex]   [pdf]   [Twelf code]  
• Mechanizing a Decision Procedure for Coproduct Equality.
  Arbob Ahmad and Daniel R. Licata and Robert Harper.
  Workshop on Mechanizing Metatheory, 2007.
  [slides pdf]
• Subtyping and Intersection Types Revisited.
  Frank Pfenning.
  Invited talk at the International Conference on Functional Programming, 2007.
  [abstract pdf]   [slides pdf]
• A Pronominal Account of Binding and Computation.
  Robert Harper.
  Invited talk at TAASN, 2009.
  [slides pdf]
• A Focusing on Binding and Computation.
  Robert Harper.
  Invited talk at TLCA/RTA, 2009.
  [slides pdf]

Events Organized

• The Twelf Tutorial, co-located with POPL 2009.
• Mechanizing Metatheory Using LF and Twelf course at the University of Oregon Summer School on Logic and Theorem Proving in Programming Languages, 2008.

Support

This research was sponsored in part by the National Science Foundation under grant number CCF-0702381, Collaborative Research: Integrating Types and Verification. The views and conclusions contained in this document are those of the author and should not be interpreted as representing the official policies, either expressed or implied, of any sponsoring institution, the U.S. government or any other entity.