DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2020.28

Strongly Normalizing Higher-Order Relational Queries

Authors: Wilmer Ricciotti and James Cheney

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract

Language-integrated query is a powerful programming construct allowing database queries and ordinary program code to interoperate seamlessly and safely. Language-integrated query techniques rely on classical results about monadic comprehension calculi, including the conservativity theorem for nested relational calculus. Conservativity implies that query expressions can freely use nesting and unnesting, yet as long as the query result type is a flat relation, these capabilities do not lead to an increase in expressiveness over flat relational queries. Wong showed how such queries can be translated to SQL via a constructive rewriting algorithm, and Cooper and others advocated higher-order nested relational calculi as a basis for language-integrated queries in functional languages such as Links and F#. However there is no published proof of the central strong normalization property for higher-order nested relational queries: a previous proof attempt does not deal correctly with rewrite rules that duplicate subterms. This paper fills the gap in the literature, explaining the difficulty with a previous proof attempt, and showing how to extend the ⊤⊤-lifting approach of Lindley and Stark to accommodate duplicating rewrites. We also sketch how to extend the proof to a recently-introduced calculus for heterogeneous queries mixing set and multiset semantics.

Cite as

Wilmer Ricciotti and James Cheney. Strongly Normalizing Higher-Order Relational Queries. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 28:1-28:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{ricciotti_et_al:LIPIcs.FSCD.2020.28,
  author =	{Ricciotti, Wilmer and Cheney, James},
  title =	{{Strongly Normalizing Higher-Order Relational Queries}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{28:1--28:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.28},
  URN =		{urn:nbn:de:0030-drops-123506},
  doi =		{10.4230/LIPIcs.FSCD.2020.28},
  annote =	{Keywords: Strong normalization, ⊤⊤-lifting, Nested relational calculus, Language-integrated query}
}

Document

DOI: 10.4230/LIPIcs.CSL.2017.36

Strongly Normalizing Audited Computation

Authors: Wilmer Ricciotti and James Cheney

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract

Auditing is an increasingly important operation for computer programming, for example in security (e.g. to enable history-based access control) and to enable reproducibility and accountability (e.g. provenance in scientific programming). Most proposed auditing techniques are ad hoc or treat auditing as a second-class, extralinguistic operation; logical or semantic foundations for auditing are not yet well-established. Justification Logic (JL) offers one such foundation; Bavera and Bonelli introduced a computational interpretation of JL called lambda^h that supports auditing. However, lambda^h is technically complex and strong normalization was only established for special cases. In addition, we show that the equational theory of lambda^h is inconsistent. We introduce a new calculus lambda^hc that is simpler than lambda^hc, consistent, and strongly normalizing. Our proof of strong normalization is formalized in Nominal Isabelle.

Cite as

Wilmer Ricciotti and James Cheney. Strongly Normalizing Audited Computation. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 36:1-36:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{ricciotti_et_al:LIPIcs.CSL.2017.36,
  author =	{Ricciotti, Wilmer and Cheney, James},
  title =	{{Strongly Normalizing Audited Computation}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{36:1--36:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.36},
  URN =		{urn:nbn:de:0030-drops-76817},
  doi =		{10.4230/LIPIcs.CSL.2017.36},
  annote =	{Keywords: lambda calculus, justification logic, strong normalization, audited computation}
}

Search Results

Documents authored by Ricciotti, Wilmer

Strongly Normalizing Higher-Order Relational Queries

Abstract

Cite as

Strongly Normalizing Audited Computation

Abstract

Cite as

Thanks for your feedback!

Could not send message