## 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.

- 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.

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.