Now showing items 1-8 of 8

    • Certified Web Services in Ynot 

      Wisnesky, Ryan; Malecha, Gregory Michael; Morrisett, John Gregory (2010-04-21)
      In this paper we demonstrate that it is possible to implement certi ed web systems in a way not much di erent from writing Standard ML or Haskell code, including use of imperative features like pointers, les, and socket ...
    • Compositional Computational Reflection 

      Malecha, Gregory Michael; Chlipala, Adam; Baibant, Thomas (Springer Science + Business Media, 2014)
      Current work on computational reflection is single-minded; each reflective procedure is written with a specific application or scope in mind. Composition of these reflective procedures is done by a proof- generating tactic ...
    • 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 ...
    • Extensible Proof Engineering in Intensional Type Theory 

      Malecha, Gregory (2015-02-24)
      We increasingly rely on large, complex systems in our daily lives---from the computers that park our cars to the medical devices that regulate insulin levels to the servers that store our personal information in the cloud. ...
    • Mechanized Verification with Sharing 

      Malecha, Gregory Michael; Morrisett, John Gregory (Springer Verlag, 2010)
      We consider software verification of imperative programs by theorem proving in higher-order separation logic. Separation logic is quite effective for reasoning about tree-like data structures, but less so for data structures ...
    • A More Precise Security Type System for Dynamic Security Tests 

      Malecha, Gregory Michael; Chong, Stephen N (2010)
      The move toward publically available services that store private information has increased the importance of tracking information flow in applications. For example, network systems that store credit-card transactions and ...
    • Preliminary Design of the SAFE Platform 

      Morrisett, John Gregory; DeHon, André; Karel, Ben; Malecha, Gregory Michael; Montagu, Benoît; Morisset, Robin; Pierce, Benjamin C.; Pollack, Randy; Ray, Sumit; Shivers, Olin; Smith, Jonathan M.; Sullivan, Gregory; Knight, Thomas F., Jr. (Association for Computing Machinery, 2011)
      SAFE is a clean-slate design for a secure host architecture. It integrates advances in programming languages, operating systems, and hardware and incorporates formal methods at every step. Though the project is still at ...
    • 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 ...