-
Notifications
You must be signed in to change notification settings - Fork 0
/
index.html
297 lines (268 loc) · 11.7 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<meta http-equiv="X-UA-Compatible" content="IE=edge">
<meta name="viewport" content="width=device-width, initial-scale=1">
<!-- The above 3 meta tags *must* come first in the head; any other head content must come *after* these tags -->
<meta name="description" content="">
<meta name="author" content="">
<title>Q*cert</title>
<!-- Bootstrap core CSS -->
<link href="./bootstrap/css/bootstrap.min.css" rel="stylesheet">
<!-- Bootstrap theme -->
<link href="./bootstrap/css/bootstrap-theme.min.css" rel="stylesheet">
<!-- Custom styles for this template -->
<link href="qcertsite.css" rel="stylesheet">
</head>
<body>
<div class="container theme-showcase" role="main">
<!-- Static navbar -->
<nav class="navbar navbar-default">
<div class="navbar-header">
<button type="button" class="navbar-toggle collapsed" data-toggle="collapse" data-target="#navbar" aria-expanded="false" aria-controls="navbar">
<span class="sr-only">Toggle navigation</span>
<span class="icon-bar"></span>
<span class="icon-bar"></span>
<span class="icon-bar"></span>
</button>
<a class="navbar-brand" href="index.html">Q*cert</a>
</div>
<div class="container-fluid">
<div id="navbar" class="navbar-collapse collapse">
<ul class="nav navbar-nav">
<li class="active"><a href="index.html">Home</a></li>
<li><a href="doc.html">Commented Code</a></li>
<li><a href="demo.html">Demo</a></li>
</ul>
<ul class="nav navbar-nav navbar-right">
<li><a href="http://github.com/querycert/qcert">github</a></li>
</ul>
</div><!--/.nav-collapse -->
</div><!--/.container-fluid -->
</nav>
<!-- ============ Body ============ -->
<!-- Main jumbotron for a primary marketing message or call to action -->
<div class="jumbotron">
<img class="img-responsive pull-right" src="qcert-logo.png" width="120" alt="Q*cert"/>
<h2>Q*cert</h2>
<p>
A query compiler written using
the <a href="https://coq.inria.fr">Coq proof assistant</a><br>
and a platform for implementing and verifying query compilers.
</p>
<div id="content" class="row spaced">
<div class="col-md-4">
<p>
<a class="btn btn-default btn-lg fixed-size"
href="http://github.com/querycert/qcert">
Get the code
</a>
</p>
</div>
<div class="col-md-4">
<p>
<a class="btn btn-default btn-lg fixed-size"
href="demo.html">
Try it online
</a>
</p>
</div>
<!--
<div class="col-md-4">
<p>
<a class="btn btn-default btn-lg btn-warning fixed-size"
href="../qcert/www/demo.html">
SIGMOD'2017 Demo
</a>
</p>
</div>
-->
</div>
</div><!--/.jumbotron -->
<h3>What is Q*cert?</h3>
<p>
Q*cert is a query compiler: it takes some input query and generates
code for execution. It can compile several source query languages,
such as (subsets of) SQL and OQL. It can produce code for several
target backends, such as Java, JavaScript, Cloudant and Spark.
</p>
<p>
Q*cert implements several intermediate languages useful for
compilation and optimization. The semantics of each of them is
precisely defined using the Coq proof assistant. Using Coq allows to
prove properties on these languages, to verify the correctness of
the translation from one to another, and to check that optimizations
are correct.
</p>
<p>
An architecture made of small and well defined components makes
Q*cert a promising platform for implementing or verifying new query
languages and to develop new optimizations.
</p>
<h3>Q*cert Specification</h3>
<p>
The code for the compiler is available as open-source
on <a href="https://github.com/querycert/qcert">github</a>.
</p>
<p>
The compiler architecture and the compilation paths are discribed in
the <a href="html/Qcert.Compiler.Driver.CompDriver.html#driver">compiler
driver</a> and can be represented by the following figure:
</p>
<object id="compilation" data="figure/figure.svg" type="image/svg+xml"
width="700"><img src="figure/figure.png" alt="Compilation Paths" width="700"/></object>
<p>
The supported languages are:
<ul>
<li><a href="html/Qcert.TechRule.Lang.TechRule.html">TechRule</a>: ODM technical rules</li>
<li><a href="html/Qcert.DesignRule.Lang.DesignRule.html">DesignerRule</a>: ODM designer rules</li>
<li><a href="html/Qcert.CAMPRule.Lang.CAMPRule.html">CAMPRule</a>: Rule Macros for CAMP</li>
<li><a href="html/Qcert.LambdaNRA.Lang.LambdaNRA.html">𝝀-NRA</a>: Lambda NRA</li>
<li><a href="html/Qcert.SQL.Lang.SQL.html">SQL</a>: Structured Query Language</li>
<li><a href="html/Qcert.SQLPP.Lang.SQLPP.html">SQL++</a>: Structured Query Language extended for JSON</li>
<li><a href="html/Qcert.OQL.Lang.OQL.html">OQL</a>: Object Query Language</li>
<li><a href="html/Qcert.CAMP.Lang.CAMP.html">CAMP</a>: Calculus of Aggregating Matching Patterns</li>
<li><a href="html/Qcert.NRA.Lang.NRA.html">NRA</a>: Nested Relational Algebra</li>
<li><a href="html/Qcert.NRAEnv.Lang.NRAEnv.html">NRA<sup>e</sup></a>: NRA with Environments</li>
<li><a href="html/Qcert.cNRAEnv.Lang.cNRAEnv.html">cNRA<sup>e</sup></a>: Core NRA<sup>e</sup></li>
<li><a href="html/Qcert.NNRC.Lang.NNRC.html">NNRC</a>: Named Nested Relational Calculus</li>
<li><a href="html/Qcert.cNNRC.Lang.cNNRC.html">cNNRC</a>: Core NNRC</li>
<li><a href="html/Qcert.NNRS.Lang.NNRS.html">NNRS</a>: Lightly Imperative NNRC</li>
<li><a href="html/Qcert.DNNRC.Lang.DNNRC.html">DNNRC</a>: Distributed NNRC</li>
<li><a href="html/Qcert.tDNNRC.Lang.tDNNRC.html">tDNNRC</a>: Typed DNNRC</li>
<li><a href="html/Qcert.NNRCMR.Lang.NNRCMR.html">NNRCMR</a>: NNRC extended with Map/Reduce</li>
<li><a href="html/Qcert.CldMR.Lang.CldMR.html">CldMR</a>: NNRC extended with Map/Reduce for Cloudant</li>
</ul>
</p>
<h3>Publications</h3>
<p>
Additional information on some of the novel aspects of the Q*cert
work can be found in research publications:
<p>
<ul>
<li>
The Q*cert compiler was originally developed as part of the
project <a href="https://doi.org/10.1147/JRD.2016.2527419">META:
Middleware for Events, Transactions, and Analytics</a> (IBM
Journal of Research and Development).
</li>
<li>
The Calculus for Aggregating Matching Patterns (CAMP) and its
translation to NRA and NNRC were first presented
in: <emph><a href="http://drops.dagstuhl.de/opus/volltexte/2015/5237/">A
Pattern Calculus for Rule Languages: Expressiveness,
Compilation, and Mechanization</a></emph>, Avraham Shinnar,
Jerome Simeon and Martin Hirzel,
ECOOP'2015. (<a href="slides/CAMP-ecoop15.pdf">slides</a>).
</li>
<li>
A description for the Q*cert type system, which handles classes
and inheritance, was first presented
in: <emph><a href="http://rd.springer.com/chapter/10.1007/978-3-319-30936-1_20?cm_mc_uid=18475580378714936652973&cm_mc_sid_50200000=">A
Branding Strategy for Business Types</a></emph>, Avraham
Shinnar, Jerome Simeon, in "A List of Successes That Can Change
the World - Essays Dedicated to Philip Wadler on the Occasion of
His 60th Birthday", pp 367-387.
</li>
<li>
Details on our experience prototyping a query compiler for
business rules aggregations can be found in: <emph>Prototyping a
Query Compiler Using Coq (Experience Report)</emph>, Joshua
Auerbach, Martin Hirzel, Louis Mandel, Avraham Shinnar and
Jerome Simeon, ACM SIGPLAN ICFP'2017
conference. (<a href="slides/icfp17-slides.pdf">slides</a>).
</li>
<li>
A French version of that same article is also available
in: <emph><a href="papers/jfla2017.pdf">Prototyper un
compilateur de requêtes avec Coq</a></emph>, Joshua Auerbach,
Martin Hirzel, Louis Mandel, Avraham Shinnar and Jerome Simeon,
JFLA'2017. (<a href="slides/jfla2017.pdf">slides</a>).
</li>
<li>
Details on the extension to the Nested Relational Algebra used
in Q*cert and on its algebraic optimizer can be found in:
<emph><a href="http://hirzels.com/martin/papers/sigmod17-nra-env.pdf">Handling
Environments in a Nested Relational Algebra with Combinators and
an Implementation in a Verified Query Compiler</a></emph>,
Joshua Auerbach, Martin Hirzel, Louis Mandel, Avraham Shinnar
and Jerome Simeon, ACM SIGMOD'2017
conference. (<a href="slides/sigmod2017.pdf">slides</a>).
</li>
<li>
A description for a full demonstration of the system can be
found
in: <emph><a href="http://hirzels.com/martin/papers/sigmod17-qcert.pdf">Q*cert:
A Platform for Implementing and Verifying Query
Compilers</a></emph>, by Joshua Auerbach, Martin Hirzel, Louis
Mandel, Avraham Shinnar and Jerome Simeon, ACM SIGMOD'2017
conference. (<a href="slides/qcert-poster.pdf">poster</a>).
</li>
</ul>
<h3>Related Projects</h3>
<p>
Applying formal verification techniques to query languages and
compilers is an active research area. The following projects
have close connections with our work:
</p>
<ul>
<li>
Gregory Malecha and Ryan Wisnesky have recently developed
techniques for <a href="http://wisnesky.net/dbpl15.pdf">semantics
optimization of language integrated queries</a> using the Coq
proof assistant.
</li>
<li>
Veronique Benzaken, Evelyne Contejean, and Stefania Dumbrava have
developed
a <a href="https://www.lri.fr/~benzaken/papers/esop14.pdf">A
Coq Formalization of the Relational Data Model</a> as part
of the <a href="https://vals.lri.fr/contracts.html">Datacert
project</a>.
</li>
<li>
James Cheney and Christian Urban have developed a mechanization
for a subset of XQuery, the XML query language
in <a href="http://homepages.inf.ed.ac.uk/jcheney/projects/XQuery/">Mechanizing
the metatheory of mini-XQuery</a>.
</li>
<li>
Some earlier work on building a verified relational database was
presented
in <a href="http://ynot.cs.harvard.edu/papers/popl10.pdf">Toward
a Verified Relational Database Management System</a> by
Gregory Malecha, Greg Morrisett, Avraham Shinnar and Ryan
Wisnesky.
</li>
<li>
To the best of our knowledge, the first attempt at applying
theorem proving technology to query compilers was done as
part of
the <a href="http://www.cs.brandeis.edu/~cokokola/">Coko-Kola</a>
project, using
the <a href="http://www.sds.lcs.mit.edu/spd/larch/index.html">Larch
theorem prover</a>.
</li>
</ul>
<h3>Credits</h3>
<p>
Q*cert initial source code was developed at the IBM T.J. Watson
Research Center by Josh Auerbach, Stefan Fehrenbach, Martin Hirzel,
Louis Mandel, Avraham Shinnar and
<a href="http://researcher.watson.ibm.com/person/us-simeon">Jerome
Simeon</a>.
</p>
<!-- ============================== -->
</div>
<!-- Bootstrap core JavaScript
================================================== -->
<!-- Placed at the end of the document so the pages load faster -->
<script src="https://ajax.googleapis.com/ajax/libs/jquery/1.12.4/jquery.min.js"></script>
<script>window.jQuery || document.write('<script src="./assets/js/vendor/jquery.min.js"><\/script>')</script>
<script src="./bootstrap/js/bootstrap.min.js"></script>
<script src="./assets/js/docs.min.js"></script>
<!-- IE10 viewport hack for Surface/desktop Windows 8 bug -->
<script src="./assets/js/ie10-viewport-bug-workaround.js"></script>
</body>
</html>