DARTS.1.1.8.pdf
- Filesize: 338 kB
- 2 pages
Document
A Pattern Calculus for Rule Languages: Expressiveness, Compilation, and Mechanization (Artifact)
Authors
-
Part of:
Issue:
Special Issue of the 29th European Conference on Object-Oriented Programming (ECOOP 2015)
Volume: DARTS, Volume 1 (ECOOP 2015)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS) - License:
Creative Commons Attribution 3.0 Germany license
- Publication Date: 2015-10-30
Cite As Get BibTex
Avraham Shinnar, Jérôme Siméon, and Martin Hirzel. A Pattern Calculus for Rule Languages: Expressiveness, Compilation, and Mechanization (Artifact). In Special Issue of the 29th European Conference on Object-Oriented Programming (ECOOP 2015). Dagstuhl Artifacts Series (DARTS), Volume 1, Issue 1, pp. 8:1-8:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/DARTS.1.1.8
Artifact
darts-v001-i001-08-artifact-24e0a0d6b258565630a5e372039cbf44.zip
(Filesize: 388 kB)
MD5 Sum:
24e0a0d6b258565630a5e372039cbf44
(Get MD5 Sum)
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.
Subject Classification
Keywords
- Rules
- Pattern Matching
- Aggregation
- Nested Queries
- Mechanization
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Coq reference manual, version 8.4pl41. URL: http://coq.inria.fr/.