Now showing items 1-7 of 7

    • 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 ...
    • 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 ...
    • Functional Query Languages with Categorical Types 

      Wisnesky, Ryan (2014-02-25)
      We study three category-theoretic types in the context of functional query languages (typed lambda-calculi extended with additional operations for bulk data processing). The types we study are:
    • Mapping Dependence 

      Wisnesky, Ryan (2009)
      We describe DMSL, a domain specific language for defining schema mappings. Schema mappings are assertions in carefully crafted logics that express constraints between data represented in different formats, including XML ...
    • Mapping Polymorphism - Proofs 

      Wisnesky, Ryan; Hernandez, Mauricio A.; Popa, Lucian (2009)
      This technical report contains the proofs for the paper Mapping Polymorphism, by Ryan Wisnesky, Mauricio A. Hernandez, and Lucian Popa, which appears in the proceedings of the 13th International Conference on Database ...
    • Minimizing Monad Comprehensions 

      Wisnesky, Ryan (2011)
      Monad comprehensions are by now a mainstay of functional programming languages. In this paper we develop a theory of semantic optimization for monad comprehensions that goes beyond rewriting using the monad laws. A ...
    • 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 ...