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.
Keywords for this software
References in zbMATH (referenced in 35 articles , 1 standard article )
Showing results 1 to 20 of 35.
Sorted by year (- Charguéraud, Arthur; Pottier, François: Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits (2019)
- Lammich, Peter: Refinement to imperative HOL (2019)
- Sakaguchi, Kazuhiko: Program extraction for mutable arrays (2018)
- Swierstra, Wouter; Alpuim, Joao: From proposition to program. Embedding the refinement calculus in Coq (2016)
- Jacobs, Bart: Dijkstra and Hoare monads in monadic computation (2015)
- Paulin-Mohring, Christine: Introduction to the calculus of inductive constructions (2015)
- Penninckx, Willem; Jacobs, Bart; Piessens, Frank: Sound, modular and compositional verification of the input/output behavior of programs (2015)
- Ziliani, Beta; Dreyer, Derek; Krishnaswami, Neelakantan R.; Nanevski, Aleksandar; Vafeiadis, Viktor: Mtac: a monad for typed tactic programming in Coq (2015)
- Barthe, Gilles; Fournet, Cédric; Grégoire, Benjamin; Strub, Pierre-Yves; Swamy, Nikhil; Zanella-Béguelin, Santiago: Probabilistic relational verification for cryptographic implementations (2014)
- Casinghino, Chris; Sjöberg, Vilhelm; Weirich, Stephanie: Combining proofs and programs in a dependently typed language (2014)
- Jacobs, Bart: Dijkstra monads in monadic computation (2014)
- Armstrong, Alasdair; Struth, Georg; Weber, Tjark: Program analysis and verification based on Kleene algebra in Isabelle/HOL (2013)
- Benton, Nick: The proof assistant as an integrated development environment (2013) ioport
- Brady, Edwin: Programming and reasoning with algebraic effects and dependent types (2013)
- Charlton, Nathaniel; Reus, Bernhard: Specification patterns for reasoning about recursion through the store (2013)
- Li, Zhao-Peng; Zhang, Yu; Chen, Yi-Yun: A shape graph logic and a shape system (2013)
- Swamy, Nikhil; Chen, Juan; Fournet, Cédric; Strub, Pierre-Yves; Bhargavan, Karthikeyan; Yang, Jean: Secure distributed programming with value-dependent types (2013)
- Crolard, T.; Polonowski, E.: Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control (2012)
- Thamsborg, Jacob; Birkedal, Lars; Yang, Hongseok: Two for the price of one: lifting separation logic assertions (2012)
- Gibbons, Jeremy; Hinze, Ralf: Just do it: simple monadic equational reasoning (2011)