A Pattern Calculus for Rule Languages: Expressiveness, Compilation, and Mechanization (Artifact)

Authors Avraham Shinnar, Jérôme Siméon, Martin Hirzel



PDF
Thumbnail PDF

Artifact Description

DARTS.1.1.8.pdf
  • Filesize: 338 kB
  • 2 pages

Document Identifiers

Author Details

Avraham Shinnar
Jérôme Siméon
Martin Hirzel

Cite AsGet 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

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.
Keywords
  • Rules
  • Pattern Matching
  • Aggregation
  • Nested Queries
  • Mechanization

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Coq reference manual, version 8.4pl41. URL: http://coq.inria.fr/.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail