The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

We would like to announce the first official release of the Ynot 
library, available at:
   http://ynot.cs.harvard.edu/

Ynot is a library for Coq 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.

P.S.: We've been developing under Coq 8.1 and recently learned that our 
build process runs into an infinite loop in Coq 8.2.  We'd be really 
grateful for any patch that someone might come up with to get things 
working with 8.2.