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)