Search Results

Documents authored by Cheney, James

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}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2017.12
muPuppet: A Declarative Subset of the Puppet Configuration Language

Authors: Weili Fu, Roly Perera, Paul Anderson, and James Cheney

Published in: LIPIcs, Volume 74, 31st European Conference on Object-Oriented Programming (ECOOP 2017)

Abstract
Puppet is a popular declarative framework for specifying and managing complex system configurations. The Puppet framework includes a domain-specific language with several advanced features inspired by object-oriented programming, including user-defined resource types, ‘classes’ with a form of inheritance, and dependency management. Like most real-world languages, the language has evolved in an ad hoc fashion, resulting in a design with numerous features, some of which are complex, hard to understand, and difficult to use correctly. We present an operational semantics for muPuppet, a representative subset of the Puppet language that covers the distinctive features of Puppet, while excluding features that are either deprecated or work-in-progress. Formalising the semantics sheds light on difficult parts of the language, identifies opportunities for future improvements, and provides a foundation for future analysis or debugging techniques, such as static typechecking or provenance tracking. Our semantics leads straightforwardly to a reference implementation in Haskell. We also discuss some of Puppet’s idiosyncrasies, particularly its handling of classes and scope, and present an initial corpus of test cases supported by our formal semantics.
Cite as

Weili Fu, Roly Perera, Paul Anderson, and James Cheney. muPuppet: A Declarative Subset of the Puppet Configuration Language. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 12:1-12:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{fu_et_al:LIPIcs.ECOOP.2017.12,
  author =	{Fu, Weili and Perera, Roly and Anderson, Paul and Cheney, James},
  title =	{{muPuppet: A Declarative Subset of the Puppet Configuration Language}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  pages =	{12:1--12:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-035-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{74},
  editor =	{M\"{u}ller, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.12},
  URN =		{urn:nbn:de:0030-drops-72656},
  doi =		{10.4230/LIPIcs.ECOOP.2017.12},
  annote =	{Keywords: configuration languages, Puppet, operational semantics}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.18
Causally Consistent Dynamic Slicing

Authors: Roly Perera, Deepak Garg, and James Cheney

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
We offer a lattice-theoretic account of the problem of dynamic slicing for pi-calculus, building on prior work in the sequential setting. For any particular run of a concurrent program, we exhibit a Galois connection relating forward and backward slices of the initial and terminal configurations. We prove that, up to lattice isomorphism, the same Galois connection arises for any causally equivalent execution, allowing an efficient concurrent implementation of slicing via a standard interleaving semantics. Our approach has been formalised in the dependently-typed programming language Agda.
Cite as

Roly Perera, Deepak Garg, and James Cheney. Causally Consistent Dynamic Slicing. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 18:1-18:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{perera_et_al:LIPIcs.CONCUR.2016.18,
  author =	{Perera, Roly and Garg, Deepak and Cheney, James},
  title =	{{Causally Consistent Dynamic Slicing}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{18:1--18:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.18},
  URN =		{urn:nbn:de:0030-drops-61584},
  doi =		{10.4230/LIPIcs.CONCUR.2016.18},
  annote =	{Keywords: pi-calculus; dynamic slicing; causal equivalence; Galois connection}
}
Document
DOI: 10.4230/DagRep.4.12.48
Programming Languages for Big Data (PlanBig) (Dagstuhl Seminar 14511)

Authors: James Cheney, Torsten Grust, and Dimitrios Vytiniotis

Published in: Dagstuhl Reports, Volume 4, Issue 12 (2015)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 14511 "Programming Languages for Big Data (PlanBig)". The seminar was motivated by recent developments in programming languages, databases, machine learning, and cloud computing, and particularly by the opportunities offered by research drawing on more than one of these areas. Participants included researchers working in each of these areas and several who have previously been involved in research in the intersection of databases and programming languages. The seminar included talks, demos and free time for discussion or collaboration. This report collects the abstracts of talks and other activities, a summary of the group discussions at the seminar, and a list of outcomes.
Cite as

James Cheney, Torsten Grust, and Dimitrios Vytiniotis. Programming Languages for Big Data (PlanBig) (Dagstuhl Seminar 14511). In Dagstuhl Reports, Volume 4, Issue 12, pp. 48-67, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{cheney_et_al:DagRep.4.12.48,
  author =	{Cheney, James and Grust, Torsten and Vytiniotis, Dimitrios},
  title =	{{Programming Languages for Big Data (PlanBig) (Dagstuhl Seminar 14511)}},
  pages =	{48--67},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{4},
  number =	{12},
  editor =	{Cheney, James and Grust, Torsten and Vytiniotis, Dimitrios},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.4.12.48},
  URN =		{urn:nbn:de:0030-drops-50055},
  doi =		{10.4230/DagRep.4.12.48},
  annote =	{Keywords: Programming languages, databases, data-centric computation, machine learning, cloud computing}
}
Document
DOI: 10.4230/DagRep.2.2.84
Principles of Provenance (Dagstuhl Seminar 12091)

Authors: James Cheney, Anthony Finkelstein, Bertram Ludaescher, and Stijn Vansummeren

Published in: Dagstuhl Reports, Volume 2, Issue 2 (2012)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 12091 ``Principles of Provenance''. The term ``provenance'' refers to information about the origin, context, derivation, ownership or history of some artifact. In both art and science, provenance information is crucial for establishing the value of a real-world artifact, guaranteeing for example that the artifact is an original work produced by an important artist, or that a stated scientific conclusion is reproducible. Since it is much easier to copy or alter digital information than it is to copy or alter real-world artifacts, the need for tracking and management of provenance information to testify the value and correctness of digital information has been firmly established in the last few years. As a result, provenance tracking and management has been studied in many settings, ranging from databases, scientific workflows, business process modeling, and security to social networking and the Semantic Web, but with relatively few interaction between these areas. This Dagstuhl seminar has focused on bringing together researchers from the above and other areas to identify the commonalities and differences of dealing with provenance; improve the mutual understanding of these communities; and identify main areas for further foundational provenance research.
Cite as

James Cheney, Anthony Finkelstein, Bertram Ludaescher, and Stijn Vansummeren. Principles of Provenance (Dagstuhl Seminar 12091). In Dagstuhl Reports, Volume 2, Issue 2, pp. 84-113, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@Article{cheney_et_al:DagRep.2.2.84,
  author =	{Cheney, James and Finkelstein, Anthony and Ludaescher, Bertram and Vansummeren, Stijn},
  title =	{{Principles of Provenance (Dagstuhl Seminar 12091)}},
  pages =	{84--113},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2012},
  volume =	{2},
  number =	{2},
  editor =	{Cheney, James and Finkelstein, Anthony and Ludaescher, Bertram and Vansummeren, Stijn},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.2.2.84},
  URN =		{urn:nbn:de:0030-drops-35073},
  doi =		{10.4230/DagRep.2.2.84},
  annote =	{Keywords: Provenance, Lineage, Metadata, Trust, Repeatability, Accountability}
}
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact