Q*cert Publications
2017
Handling Environments in a Nested Relational Algebra with Combinators and an Implementation in a Verified Query Compiler
Auerbach, Joshua and Hirzel, Martin and Mandel, Louis and Shinnar, Avi and Simeon, Jerome
Proceedings of the ACM International Conference on Management of Data (SIGMOD), 2017
Abstract
Algebras based on combinators, i.e., variable-free, have been
proposed as a better representation for query compilation and
optimization. A key benefit of combinators is that they avoid the
need to handle variable shadowing or accidental capture during
rewrites. This simplifies both the optimizer specification and its
correctness analysis, but the environment from the source language
has to be reified as records, which can lead to more complex query
plans.
This paper proposes NRAEnv, an extension of a combinators-based
nested relational algebra (NRA) with built-in support for
environments. We show that it can naturally encode an equivalent NRA
with lambda terms and that all optimizations on NRA carry over to
NRAEnv. This extension provides an elegant way to represent views
in query plans, and can radically simplify compilation and
optimization for source languages with rich environment
manipulations.
We have specified a query compiler using the Coq proof assistant
with NRAEnv at its heart. Most of the compiler, including the query
optimizer, is accompanied by a (machine-checked) correctness
proof. The implementation is automatically extracted from the
specification, resulting in a query compiler with a verified core.
Q* cert: A Platform for Implementing and Verifying Query Compilers
Joshua S Auerbach and Martin Hirzel and Louis Mandel and Avraham Shinnar and Jérôme Siméon
Proceedings of the ACM International Conference on Management of Data (SIGMOD), pp. 1703--1706, 2017
Abstract
We present Q*cert, a platform for the specification, verification,
and implementation of query compilers written using the Coq proof
assistant. The Q*cert platform is open source and includes some
support for SQL and OQL, and for code generation to Spark and
Cloudant. It internally relies on familiar database intermediate
representations, notably the nested relational algebra and calculus
and a novel extension of the nested relational algebra that eases
the handling of environments. The platform also comes with simple
but functional and extensible query optimizers.
We demonstrate how the platform can be used to implement a compiler
for a new input language or develop new optimizations that can be
formally verified. We also demonstrate a web-based interface that
allows the developer to explore various compilation and optimization
strategies.
Prototyping a query compiler using Coq (experience report)
Auerbach, Joshua S and Hirzel, Martin and Mandel, Louis and Shinnar, Avraham and Simeon, Jerome
Proceedings of the ACM on Programming Languages 1(ICFP), 9, ACM, 2017
Abstract
Designing and prototyping new features is important in many industrial
projects. Functional programming and formal verification tools can
prove valuable for that purpose, but lead to challenges when
integrating with existing product code or when planning technology
transfer.
This article reports on our experience using the Coq proof
assistant as a prototyping environment for building a query compiler
intended for use in IBM's ODM Insights product. We discuss the pros and cons of
using Coq for this purpose and describe our methodology for porting the
compiler to Java, as required for product integration.
2016
A Branding Strategy for Business Types
Avraham Shinnar, Jerome Simeon
A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, pp. 367--387, 2016
Abstract
In the course of building a compiler from business rules to a
database run-time, we encounter the need for a type system that
includes a class hierarchy and subtyping in the presence of complex
record operations. Since our starting point is based on structural
typing and targets a data-centric language, we develop an approach
inspired by Wadler's work on XML types. Our
proposed type system has strong similarities with branded or tagged
objects, combining nominal and structural typing, and is designed to
support a rich set of operations on records commonly found in
database languages. We show soundness of the type system and
illustrate its use on two of the intermediate languages involved in
our compiler for business rules: a calculus for pattern matching
with aggregation (CAMP) that captures rules semantics, and the
nested relational algebra (NRA) used for optimization and code
generation. We show type soundness for both languages. The approach
and correctness proofs are fully mechanized using the Coq
proof-assistant.
2015
A Pattern Calculus for Rule Languages: Expressiveness, Compilation, and Mechanization (Artifact)
Avraham Shinnar, Jerome Simeon, Martin Hirzel
DARTS 1(1), 08:1--08:2, 2015
Abstract
This artifact contains the accompanying code for the ECOOP 2015 paper: "A Pattern Calculus for Rule Languages: Expressiveness, Compilation, and Mechanization". It contains source files for a full mechanization of the three languages presented in the paper: CAMP (Calculus for Aggregating Matching Patterns), NRA (Nested Relational Algebra) and NNRC (Named Nested Relational Calculus). Translations between all three languages and their attendant proofs of correctness are included. Additionally, a mechanization of a type system for the main languages is provided, along with bidirectional proofs of type preservation and proofs of the time complexity of the various compilers.
