Ynot

Ynot, dependent types for imperative programs. We describe an axiomatic extension to the Coq proof assistant, that supports writing, reasoning about, and extracting higher-order, dependently-typed programs with side-effects. Coq already includes a powerful functional language that supports dependent types, but that language is limited to pure, total functions. The key contribution of our extension, which we call Ynot, is the added support for computations that may have effects such as non-termination, accessing a mutable store, and throwing/catching exceptions.The axioms of Ynot form a small trusted computing base which has been formally justified in our previous work on Hoare Type Theory (HTT). We show how these axioms can be combined with the powerful type and abstraction mechanisms of Coq to build higher-level reasoning mechanisms which in turn can be used to build realistic, verified software components. To substantiate this claim, we describe here a representative series of modules that implement imperative finite maps, including support for a higher-order (effectful) iterator. The implementations range from simple (e.g., association lists) to complex (e.g., hash tables) but share a common interface which abstracts the implementation details and ensures that the modules properly implement the finite map abstraction.


References in zbMATH (referenced in 35 articles , 1 standard article )

Showing results 21 to 35 of 35.
Sorted by year (citations)
  1. Liu, Yu David; Skalka, Christian; Smith, Scott F.: Type-specialized staged programming with process separation (2011)
  2. Malecha, Gregory; Morrisett, Greg; Wisnesky, Ryan: Trace-based verification of imperative programs with I/O (2011)
  3. Schwinghammer, Jan; Birkedal, Lars; Reus, Bernhard; Yang, Hongseok: Nested Hoare triples and frame rules for higher-order store (2011)
  4. Svendsen, Kasper; Birkedal, Lars; Nanevski, Aleksandar: Partiality, state and dependent types (2011)
  5. Brady, Edwin; Hammond, Kevin: Correct-by-construction concurrency: using dependent types to verify implementations of effectful resource usage protocols (2010)
  6. Malecha, Gregory; Morrisett, Greg; Shinnar, Avraham; Wisnesky, Ryan: Toward a verified relational database management system (2010)
  7. Morgenstern, Jamie; Licata, Daniel R.: Security-typed programming within dependently typed programming (2010)
  8. Nanevski, Aleksandar; Vafeiadis, Viktor; Berdine, Josh: Structuring the verification of heap-manipulating programs (2010)
  9. Boudol, Gérard: A deadlock-free semantics for shared memory concurrency (2009)
  10. Chlipala, Adam; Malecha, Gregory; Morrisett, Greg; Shinnar, Avraham; Wisnesky, Ryan: Effective interactive proofs for higher-order imperative programs (2009)
  11. Schwinghammer, Jan; Birkedal, Lars; Reus, Bernhard; Yang, Hongseok: Nested Hoare triples and frame rules for higher-order store (2009)
  12. Swierstra, Wouter: A Hoare logic for the state monad. Proof pearl (2009)
  13. Voigtländer, Janis: Free theorems involving type constructor classes, functional pearl (2009)
  14. -: Proceedings of the 13th ACM SIGPLAN international conference on functional programming, ICFP ’08, Victoria, BC, Canada, September 20--28, 2008 (2008)
  15. Nanevski, Aleksandar; Morrisett, Greg; Shinnar, Avraham; Govereau, Paul; Birkedal, Lars: Ynot: dependent types for imperative programs (2008)