The Ynot Project

Ynot is a library for the Coq proof assistant which turns it into a full-fledged environment for writing and verifying imperative programs. In the tradition of the Haskell IO monad, Ynot axiomatizes a parameterized monad of imperative computations, where the type of a computation tells you not only what type of data it returns, but also what Hoare-logic-style precondition and postcondition it satisfies. On top of the simple axiomatic base, the library defines a separation logic. Specialized automation tactics are able to discharge automatically most proof goals about separation-style formulas that describe heaps, meaning that building a certified Ynot program is often not much harder than writing that program in Haskell.

Ynot makes it easy to enhance its automation with support for new predicates describing new data structures, and, since all such enhancements must be proved from first principles, extensibility does not require users to trust more code. All of Coq's traditional theorem-proving tools are available by default as well. Thus, Ynot enables effective proof-based software engineering, from simple memory safety of low-level imperative programs to deep correctness theorems about programs like compilers that may use imperative data structures for efficiency.

The Ynot project is supported in part by NSF Grant 0702345, entitled Collaborative Research: Integrating Types and Verification, by NSF Grant 0910660, entitled Combining Foundational and Lightweight Formal Methods to Build Certifiably Dependable Software, and by a gift from Microsoft Research.

Current Project Team

  • Adam Chlipala
  • Paul Govereau
  • Gregory Malecha
  • Greg Morrisett
  • Aleks Nanevski
  • Avi Shinnar
  • Matthieu Sozeau
  • Ryan Wisnesky
  • Past Contributors

  • Amal Ahmed
  • Lars Birkedal
  • Rasmus Lerchedahl Petersen
  • Releases

    8.3pl2 Release (NEW)
    This release contains a few small fixes for compatibility with 8.3pl2, it should also worl with 8.3pl1
    8.3pl1 Release
    This is the 8.3pl1 release of the Ynot library. Some needed functionality was lost in 8.3 that was restored in 8.3pl1 so this will not compile under regular 8.3. There may be some issues with program extraction in the webserver example.
    8.1/8.2 Release
    It is only known to work properly in Coq 8.1 and Coq 8.2pl1, but not Coq 8.2.
    Ynot RDBMS
    To fully compile it you will need Coq SVN version 12192; instructions for building Coq are here. As of March 15, 2010, ynot-rdb contains a small tweak to reduce compilation anomalies.

    Documentation and Help

  • Tutorial on basic use of the library.
  • Mailing list for users
  • Publications

    Mechanized Verification with Sharing
    Gregory Malecha, Greg Morrisett
    Proceedings of ICTAC'10

    Toward a Verified Relational Database Management System
    Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky
    Proceedings of POPL'10

    Effective Interactive Proofs for Higher-Order Imperative Programs
    Adam Chlipala, Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky
    Proceedings of ICFP'09

    Trace Based Verification of Imperative Programs with I/O
    Gregory Malecha, Greg Morrisett, and Ryan Wisnesky
    Journal of Symbolic Computation. Vol 46, issue 2.
    Automated Specification and Verification of Web Systems (Preprint)

    Certified Web Services in Ynot
    Ryan Wisnesky, Gregory Malecha, Greg Morrisett
    Proceedings of WWV'09

    Towards Type-theoretic Semantics for Transactional Concurrency
    Aleksandar Nanevski, Paul Govereau, Greg Morrisett
    Proceedings of TLDI'09
    Extended version available as technical report TR-09-07, Harvard University, July 2007.

    Ynot: Reasoning with the Awkward Squad
    Aleksandar Nanevski, Greg Morrisett, Avi Shinnar, Paul Govereau, Lars Birkedal
    Proceedings of ICFP'08
    The examples from this paper are available as a tarball that includes all of the Coq sources.

    A Realizability Model for Impredicative Hoare Type Theory
    Rasmus L. Petersen, Lars Birkedal, Aleksandar Nanevski, Greg Morrisett
    Proceedings of ESOP'08

    Hoare Type Theory, Polymorphism and Separation
    Aleksandar Nanevski, Greg Morrisett, Lars Birkedal
    Journal of Functional Programming, 18(5/6), 2008
    Extended version of the ICFP'06 paper.

    Abstract Predicates and Mutable ADTs in Hoare Type Theory
    Aleksandar Nanevski, Amal Ahmed, Greg Morrisett, Lars Birkedal
    Proceedings of ESOP'07
    Extended version available as technical report TR-14-06, Harvard University, September 2006.

    Polymorphism and Separation in Hoare Type Theory
    Aleksandar Nanevski, Greg Morrisett, Lars Birkedal
    Proceedings of ICFP'06
    Extended version available as technical report TR-10-06, Harvard University.

    Dependent Type Theory of Stateful Higher-Order Functions
    Aleksandar Nanevski, Greg Morrisett
    Extended version available as technical report TR-24-05, Harvard University.

    Talks

  • The Marriage of Dependent Types and Effects (Invited talk at TLCA'07)
  • Next Generation Type Systems (Invited talk at Microsoft Cambridge's 10th Anniversary)