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

Past Contributors

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

Publications

Talks