Now showing items 1-3 of 3

    • Effective Interactive Proofs for Higher-Order Imperative Programs 

      Chlipala, Adam J.; Malecha, Gregory Michael; Morrisett, John Gregory; Shinnar, Avraham Ever; Wisnesky, Ryan (Association for Computing Machinery, 2009)
      We present a new approach for constructing and verifying higher-order, imperative programs using the Coq proof assistant. We build on the past work on the Ynot system, which is based on Hoare Type Theory. That original ...
    • Toward a verified relational database management system 

      Malecha, Gregory Michael; Morrisett, Greg Gregory; Shinnar, Avraham; Wisnesky, Ryan (Association for Computing Machinery, 2010)
      We report on our experience implementing a lightweight, fully verified relational database management system (RDBMS). The functional specification of RDBMS behavior, RDBMS implementation, and proof that the implementation ...
    • Ynot: Dependent Types for Imperative Programs 

      Nanevski, Aleksandar; Morrisett, John Gregory; Shinnar, Avraham Ever; Govereau, Paul; Birkedal, Lars (Association for Computing Machinery, 2008)
      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 ...