Person:

Wisnesky, Ryan

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 Theory, held March 22–25, 2010, in Lausanne, Switzerland (ICDT ’10).

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:

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 monad-with-zero comprehension do x ← X; y ← Y ; if P(x, y) then return F(x, y) else zero can be rewritten, so as to minimize the number of ← bindings, using constraints that are known to hold of X and Y . The soundness of this technique varies from monad to monad, and we characterize its soundness for monads expressible in functional programming languages by generalizing classical results from relational database theory. This technique allows the optimization of a wide class of languages, ranging from large-scale data-parallel languages such as DryadLINQ and Data Parallel Haskell to robabilistic languages such as IBAL and functional-logical languages like Curry.

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 and relational schema. DMSL is suitable for representing programs over mappings, which, for instance, occur in dataflow graphs of mappings. DMSL programs of mapping type are statically guaranteed by a qualified type system to denote satisfiable constraints; the principal polymorphic schemas of source and target solution data instances are automatically inferred. DMSL implements a variety of operations over mappings (e.g., composition) by interfacing with IBM’s Clio Mapping Engine.

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 I/O. We present a web-based course gradebook application developed with Ynot, a Coq library for certi ed imperative programming.We add a dialog-based I/O system to Ynot, and we extend Ynot's underlying Hoare logic with event traces to reason about I/O be- havior. Expressive abstractions allow the modular certi cation of both high level speci cations like privacy guarantees and low level properties like memory safety and correct parsing.

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 system was a proof of concept, where every program verification was accomplished via laborious manual proofs, with much code devoted to uninteresting low-level details. In this paper, we present a re-implementation of Ynot which makes it possible to implement fully-verified, higher-order imperative programs with reasonable proof burden. At the same time, our new system is implemented entirely in Coq source files, showcasing the versatility of that proof assistant as a platform for research on language design and verification. Both versions of the system have been evaluated with case studies in the verification of imperative data structures, such as hash tables with higher-order iterators. The verification burden in our new system is reduced by at least an order of magnitude compared to the old system, by replacing manual proof with automation. The core of the automation is a simplification procedure for implications in higher-order separation logic, with hooks that allow programmers to add domain-specific simplification rules. We argue for the effectiveness of our infrastructure by verifying a number of data structures and a packrat parser, and we compare to similar efforts within other projects. Compared to competing approaches to data structure verification, our system includes much less code that must be trusted; namely, about a hundred lines of Coq code defining a program logic. All of our theorems and decision procedures have or build machine-checkable correctness proofs from first principles, removing opportunities for tool bugs to create faulty verifications.

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 meets the specification are all written and verified in Coq. Our contributions include: (1) a complete specification of the relational algebra in Coq; (2) an efficient realization of that model (B+ trees) implemented with the Ynot extension to Coq; and (3) a set of simple query optimizations that are proven to respect both semantics and run-time cost. In addition to describing the design and implementation of these artifacts, we highlight the challenges we encountered formalizing them, including the choice of representation for (finite) relations of typed tuples and the challenges of reasoning about data structures with complex sharing. Our experience shows that though many challenges remain, building fully-verified systems software in Coq is within reach.