20 Search Results for "Tannen, Val"


Volume

OASIcs, Volume 119

The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen

Tannen's Festschrift, May 24-25, 2024, University of Pennsylvania, Philadelphia, PA, USA

Editors: Antoine Amarilli and Alin Deutsch

Document
Complete Volume
OASIcs, Volume 119, Tannen's Festschrift, Complete Volume

Authors: Antoine Amarilli and Alin Deutsch

Published in: OASIcs, Volume 119, The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen (2024)


Abstract
OASIcs, Volume 119, Tannen's Festschrift, Complete Volume

Cite as

The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen. Open Access Series in Informatics (OASIcs), Volume 119, pp. 1-196, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@Proceedings{amarilli_et_al:OASIcs.Tannen,
  title =	{{OASIcs, Volume 119, Tannen's Festschrift, Complete Volume}},
  booktitle =	{The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen},
  pages =	{1--196},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-320-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{119},
  editor =	{Amarilli, Antoine and Deutsch, Alin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen},
  URN =		{urn:nbn:de:0030-drops-200953},
  doi =		{10.4230/OASIcs.Tannen},
  annote =	{Keywords: OASIcs, Volume 119, Tannen's Festschrift, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Antoine Amarilli and Alin Deutsch

Published in: OASIcs, Volume 119, The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen (2024)


Abstract
Front Matter, Table of Contents, Preface, Conference Organization

Cite as

The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen. Open Access Series in Informatics (OASIcs), Volume 119, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{amarilli_et_al:OASIcs.Tannen.0,
  author =	{Amarilli, Antoine and Deutsch, Alin},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen},
  pages =	{0:i--0:xii},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-320-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{119},
  editor =	{Amarilli, Antoine and Deutsch, Alin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.0},
  URN =		{urn:nbn:de:0030-drops-200962},
  doi =		{10.4230/OASIcs.Tannen.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Explaining Enterprise Knowledge Graphs with Large Language Models and Ontological Reasoning

Authors: Teodoro Baldazzi, Luigi Bellomarini, Stefano Ceri, Andrea Colombo, Andrea Gentili, Emanuel Sallinger, and Paolo Atzeni

Published in: OASIcs, Volume 119, The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen (2024)


Abstract
In recent times, the demand for transparency and accountability in AI-driven decisions has intensified, particularly in high-stakes domains like finance and bio-medicine. This focus on the provenance of AI-generated conclusions underscores the need for decision-making processes that are not only transparent but also readily interpretable by humans, to built trust of both users and stakeholders. In this context, the integration of state-of-the-art Large Language Models (LLMs) with logic-oriented Enterprise Knowledge Graphs (EKGs) and the broader scope of Knowledge Representation and Reasoning (KRR) methodologies is currently at the cutting edge of industrial and academic research across numerous data-intensive areas. Indeed, such a synergy is paramount as LLMs bring a layer of adaptability and human-centric understanding that complements the structured insights of EKGs. Conversely, the central role of ontological reasoning is to capture the domain knowledge, accurately handling complex tasks over a given realm of interest, and to infuse the process with transparency and a clear provenance-based explanation of the conclusions drawn, addressing the fundamental challenge of LLMs' inherent opacity and fostering trust and accountability in AI applications. In this paper, we propose a novel neuro-symbolic framework that leverages the underpinnings of provenance in ontological reasoning to enhance state-of-the-art LLMs with domain awareness and explainability, enabling them to act as natural language interfaces to EKGs.

Cite as

Teodoro Baldazzi, Luigi Bellomarini, Stefano Ceri, Andrea Colombo, Andrea Gentili, Emanuel Sallinger, and Paolo Atzeni. Explaining Enterprise Knowledge Graphs with Large Language Models and Ontological Reasoning. In The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen. Open Access Series in Informatics (OASIcs), Volume 119, pp. 1:1-1:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{baldazzi_et_al:OASIcs.Tannen.1,
  author =	{Baldazzi, Teodoro and Bellomarini, Luigi and Ceri, Stefano and Colombo, Andrea and Gentili, Andrea and Sallinger, Emanuel and Atzeni, Paolo},
  title =	{{Explaining Enterprise Knowledge Graphs with Large Language Models and Ontological Reasoning}},
  booktitle =	{The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen},
  pages =	{1:1--1:20},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-320-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{119},
  editor =	{Amarilli, Antoine and Deutsch, Alin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.1},
  URN =		{urn:nbn:de:0030-drops-200971},
  doi =		{10.4230/OASIcs.Tannen.1},
  annote =	{Keywords: provenance, ontological reasoning, language models, knowledge graphs}
}
Document
Traversal-Invariant Characterizations of Logarithmic Space

Authors: Siddharth Bhaskar, Steven Lindell, and Scott Weinstein

Published in: OASIcs, Volume 119, The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen (2024)


Abstract
We give a novel descriptive-complexity theoretic characterization of L and NL computable queries over finite structures using traversal invariance. We summarize this as (N)L = FO + (breadth-first) traversal-invariance.

Cite as

Siddharth Bhaskar, Steven Lindell, and Scott Weinstein. Traversal-Invariant Characterizations of Logarithmic Space. In The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen. Open Access Series in Informatics (OASIcs), Volume 119, pp. 2:1-2:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{bhaskar_et_al:OASIcs.Tannen.2,
  author =	{Bhaskar, Siddharth and Lindell, Steven and Weinstein, Scott},
  title =	{{Traversal-Invariant Characterizations of Logarithmic Space}},
  booktitle =	{The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen},
  pages =	{2:1--2:17},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-320-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{119},
  editor =	{Amarilli, Antoine and Deutsch, Alin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.2},
  URN =		{urn:nbn:de:0030-drops-200984},
  doi =		{10.4230/OASIcs.Tannen.2},
  annote =	{Keywords: Model theory, finite model theory, descriptive complexity theory, logarithmic space, graph traversals}
}
Document
Semiring Provenance in the Infinite

Authors: Sophie Brinke, Erich Grädel, Lovro Mrkonjić, and Matthias Naaf

Published in: OASIcs, Volume 119, The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen (2024)


Abstract
Semiring provenance evaluates database queries or logical statements not just by true or false but by values in some commutative semiring. This permits to track which combinations of atomic facts are responsible for the truth of a statement, and to derive further information, for instance concerning costs, confidence scores, number of proof trees, or access levels to protected data. The focus of this approach, proposed and developed to a large extent by Val Tannen and his collaborators, has first been on (positive) database query languages, but has later been extended, again in collaboration with Val, to a systematic semiring semantics for first-order logic (and other logical systems), as well as to a method for the strategy analysis of games. So far, semiring provenance has been studied for finite structures. To extend the semiring provenance approach for first-order logic to infinite domains, the semirings need to be equipped with addition and multiplication operators over infinite collections of values. This needs solid algebraic foundations, and we study here the necessary and desirable properties of semirings with infinitary operations to provide a well-defined and informative provenance analysis over infinite domains. We show that, with suitable definitions for such infinitary semiring, large parts of the theory of semiring provenance can be succesfully generalised to infinite structures.

Cite as

Sophie Brinke, Erich Grädel, Lovro Mrkonjić, and Matthias Naaf. Semiring Provenance in the Infinite. In The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen. Open Access Series in Informatics (OASIcs), Volume 119, pp. 3:1-3:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{brinke_et_al:OASIcs.Tannen.3,
  author =	{Brinke, Sophie and Gr\"{a}del, Erich and Mrkonji\'{c}, Lovro and Naaf, Matthias},
  title =	{{Semiring Provenance in the Infinite}},
  booktitle =	{The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen},
  pages =	{3:1--3:26},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-320-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{119},
  editor =	{Amarilli, Antoine and Deutsch, Alin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.3},
  URN =		{urn:nbn:de:0030-drops-200997},
  doi =		{10.4230/OASIcs.Tannen.3},
  annote =	{Keywords: Semiring semantics, first-order logic, semirings with infinitary operations}
}
Document
Annotation and More Annotation: Some Problems Posed by (and to) Val Tannen

Authors: Peter Buneman and Stijn Vansummeren

Published in: OASIcs, Volume 119, The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen (2024)


Abstract
Among the many research accomplishments of Val Tannen, his work on provenance and semirings is probably the most widely known. In this paper, we discuss questions that arise when applying this general framework to the setting of curated databases, and in particular the setting where we can have multiple annotations on the same data, as well as annotations on annotations.

Cite as

Peter Buneman and Stijn Vansummeren. Annotation and More Annotation: Some Problems Posed by (and to) Val Tannen. In The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen. Open Access Series in Informatics (OASIcs), Volume 119, pp. 4:1-4:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{buneman_et_al:OASIcs.Tannen.4,
  author =	{Buneman, Peter and Vansummeren, Stijn},
  title =	{{Annotation and More Annotation: Some Problems Posed by (and to) Val Tannen}},
  booktitle =	{The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen},
  pages =	{4:1--4:8},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-320-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{119},
  editor =	{Amarilli, Antoine and Deutsch, Alin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.4},
  URN =		{urn:nbn:de:0030-drops-201007},
  doi =		{10.4230/OASIcs.Tannen.4},
  annote =	{Keywords: Annotation, provenance, semiring, curated data}
}
Document
Chasing Parallelism in Aggregating Graph Queries

Authors: Alin Deutsch

Published in: OASIcs, Volume 119, The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen (2024)


Abstract
In practice, one frequently encounters queries that extract tabular results from graph databases by employing grouping and aggregation. This paper introduces a technique for rewriting the group-by list of graph queries in order to increase aggregation parallelism in graph engines that conform to a modern instantiation of the Bulk-Synchronous-Parallel computation model.

Cite as

Alin Deutsch. Chasing Parallelism in Aggregating Graph Queries. In The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen. Open Access Series in Informatics (OASIcs), Volume 119, pp. 5:1-5:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{deutsch:OASIcs.Tannen.5,
  author =	{Deutsch, Alin},
  title =	{{Chasing Parallelism in Aggregating Graph Queries}},
  booktitle =	{The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen},
  pages =	{5:1--5:14},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-320-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{119},
  editor =	{Amarilli, Antoine and Deutsch, Alin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.5},
  URN =		{urn:nbn:de:0030-drops-201011},
  doi =		{10.4230/OASIcs.Tannen.5},
  annote =	{Keywords: Graph Databases, Grouping and Aggregation, Parallel Graph Computation Models, Rewriting, Constraint-based Minimization}
}
Document
Fishing Fort: A System for Graph Analytics with ML Prediction and Logic Deduction

Authors: Wenfei Fan and Shuhao Liu

Published in: OASIcs, Volume 119, The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen (2024)


Abstract
This paper reports Fishing Fort, a graph analytic system developed in response to the following questions. What practical value can we get out of graph analytics? How can we effectively deduce the value from a real-life graph? Where can we get clean graphs to make accurate analyses possible? To answer these questions, Fishing Fort advocates to unify logic deduction and ML prediction by proposing Graph Association Rules (GARs), a class of logic rules in which ML models can be embedded as predicates. It employs GARs to deduce graph associations, enrich graphs and clean graphs. It has been deployed in production lines and proven effective in online recommendation, drug discovery, credit risk assessment, battery manufacturing and cybersecurity, among other things.

Cite as

Wenfei Fan and Shuhao Liu. Fishing Fort: A System for Graph Analytics with ML Prediction and Logic Deduction. In The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen. Open Access Series in Informatics (OASIcs), Volume 119, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{fan_et_al:OASIcs.Tannen.6,
  author =	{Fan, Wenfei and Liu, Shuhao},
  title =	{{Fishing Fort: A System for Graph Analytics with ML Prediction and Logic Deduction}},
  booktitle =	{The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen},
  pages =	{6:1--6:18},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-320-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{119},
  editor =	{Amarilli, Antoine and Deutsch, Alin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.6},
  URN =		{urn:nbn:de:0030-drops-201025},
  doi =		{10.4230/OASIcs.Tannen.6},
  annote =	{Keywords: graph analytics, data cleaning, association analysis}
}
Document
A Note on Logical PERs and Reducibility. Logical Relations Strike Again!

Authors: Jean Gallier

Published in: OASIcs, Volume 119, The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen (2024)


Abstract
We prove a general theorem for establishing properties expressed by binary relations on typed (first-order) λ-terms, using a variant of the reducibility method and logical PERs. As an application, we prove simultaneously that β-reduction in the simply-typed λ-calculus is strongly normalizing, and that the Church-Rosser property holds (and similarly for βη-reduction).

Cite as

Jean Gallier. A Note on Logical PERs and Reducibility. Logical Relations Strike Again!. In The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen. Open Access Series in Informatics (OASIcs), Volume 119, pp. 7:1-7:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{gallier:OASIcs.Tannen.7,
  author =	{Gallier, Jean},
  title =	{{A Note on Logical PERs and Reducibility. Logical Relations Strike Again!}},
  booktitle =	{The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen},
  pages =	{7:1--7:12},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-320-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{119},
  editor =	{Amarilli, Antoine and Deutsch, Alin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.7},
  URN =		{urn:nbn:de:0030-drops-201033},
  doi =		{10.4230/OASIcs.Tannen.7},
  annote =	{Keywords: Typed lambda-calculus, reducibility, logical relations, per’s, strong normalization, Church-Rosser property}
}
Document
AutoML for Explainable Anomaly Detection (XAD)

Authors: Nikolaos Myrtakis, Ioannis Tsamardinos, and Vassilis Christophides

Published in: OASIcs, Volume 119, The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen (2024)


Abstract
Numerous algorithms have been proposed for detecting anomalies (outliers, novelties) in an unsupervised manner. Unfortunately, it is not trivial, in general, to understand why a given sample (record) is labelled as an anomaly and thus diagnose its root causes. We propose the following reduced-dimensionality, surrogate model approach to explain detector decisions: approximate the detection model with another one that employs only a small subset of features. Subsequently, samples can be visualized in this low-dimensionality space for human understanding. To this end, we develop PROTEUS, an AutoML pipeline to produce the surrogate model, specifically designed for feature selection on imbalanced datasets. The PROTEUS surrogate model can not only explain the training data, but also the out-of-sample (unseen) data. In other words, PROTEUS produces predictive explanations by approximating the decision surface of an unsupervised detector. PROTEUS is designed to return an accurate estimate of out-of-sample predictive performance to serve as a metric of the quality of the approximation. Computational experiments confirm the efficacy of PROTEUS to produce predictive explanations for different families of detectors and to reliably estimate their predictive performance in unseen data. Unlike several ad-hoc feature importance methods, PROTEUS is robust to high-dimensional data.

Cite as

Nikolaos Myrtakis, Ioannis Tsamardinos, and Vassilis Christophides. AutoML for Explainable Anomaly Detection (XAD). In The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen. Open Access Series in Informatics (OASIcs), Volume 119, pp. 8:1-8:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{myrtakis_et_al:OASIcs.Tannen.8,
  author =	{Myrtakis, Nikolaos and Tsamardinos, Ioannis and Christophides, Vassilis},
  title =	{{AutoML for Explainable Anomaly Detection (XAD)}},
  booktitle =	{The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen},
  pages =	{8:1--8:23},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-320-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{119},
  editor =	{Amarilli, Antoine and Deutsch, Alin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.8},
  URN =		{urn:nbn:de:0030-drops-201049},
  doi =		{10.4230/OASIcs.Tannen.8},
  annote =	{Keywords: Anomaly Explanation, Predictive Explanation, Anomaly Interpretation, Explainable AI}
}
Document
On the Impact of Provenance Semiring Theory on the Design of a Provenance-Aware Database System

Authors: Pierre Senellart

Published in: OASIcs, Volume 119, The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen (2024)


Abstract
We report on the impact that the theory of provenance semirings, developed by Val Tannen and his collaborators, has had on the design on a practical system for maintaining the provenance of query results over a relational database, namely ProvSQL.

Cite as

Pierre Senellart. On the Impact of Provenance Semiring Theory on the Design of a Provenance-Aware Database System. In The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen. Open Access Series in Informatics (OASIcs), Volume 119, pp. 9:1-9:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{senellart:OASIcs.Tannen.9,
  author =	{Senellart, Pierre},
  title =	{{On the Impact of Provenance Semiring Theory on the Design of a Provenance-Aware Database System}},
  booktitle =	{The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen},
  pages =	{9:1--9:10},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-320-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{119},
  editor =	{Amarilli, Antoine and Deutsch, Alin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.9},
  URN =		{urn:nbn:de:0030-drops-201050},
  doi =		{10.4230/OASIcs.Tannen.9},
  annote =	{Keywords: provenance, provenance semiring, ProvSQL}
}
Document
Different Differences in Semirings

Authors: Dan Suciu

Published in: OASIcs, Volume 119, The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen (2024)


Abstract
Relational algebra operates over relations under either set semantics or bag semantics. In 2007 Val Tannen extended the semantics of relational algebra to K-relations, where each tuple is annotated with a value from a semiring. However, only the positive fragment of the relational algebra can be interpreted over K-relations. The reason is that a semiring contains only the operations addition and multiplication, and does not have a difference operation. This paper explores three ways of adding a difference operator to a semiring: as a freely generated algebra, by using the natural order, or by an explicit construction using products and quotients. The paper consists of both a survey of results from the literature, and of some novel results.

Cite as

Dan Suciu. Different Differences in Semirings. In The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen. Open Access Series in Informatics (OASIcs), Volume 119, pp. 10:1-10:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{suciu:OASIcs.Tannen.10,
  author =	{Suciu, Dan},
  title =	{{Different Differences in Semirings}},
  booktitle =	{The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen},
  pages =	{10:1--10:20},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-320-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{119},
  editor =	{Amarilli, Antoine and Deutsch, Alin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.10},
  URN =		{urn:nbn:de:0030-drops-201062},
  doi =		{10.4230/OASIcs.Tannen.10},
  annote =	{Keywords: Semirings, K-relations}
}
Document
An Intensional Expressiveness Gap of Comprehension Syntax

Authors: Limsoon Wong

Published in: OASIcs, Volume 119, The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen (2024)


Abstract
Comprehension syntax is widely adopted in modern programming languages as a means for manipulating collection types. This paper proves that all subquadratic algorithms which are expressible in comprehension syntax, do not compute low-selectivity joins. As database systems support these joins efficiently, this confirms an intensional expressiveness gap between comprehension syntax and relational database systems. The proof of this intensional expressiveness gap relies on a "limited-mixing" lemma which states that subquadratic algorithms expressible using comprehension syntax have limited ability for mixing atomic objects in their inputs.

Cite as

Limsoon Wong. An Intensional Expressiveness Gap of Comprehension Syntax. In The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen. Open Access Series in Informatics (OASIcs), Volume 119, pp. 11:1-11:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{wong:OASIcs.Tannen.11,
  author =	{Wong, Limsoon},
  title =	{{An Intensional Expressiveness Gap of Comprehension Syntax}},
  booktitle =	{The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen},
  pages =	{11:1--11:13},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-320-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{119},
  editor =	{Amarilli, Antoine and Deutsch, Alin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Tannen.11},
  URN =		{urn:nbn:de:0030-drops-201074},
  doi =		{10.4230/OASIcs.Tannen.11},
  annote =	{Keywords: Comprehension syntax, intensional expressive power, limited-mixing lemma}
}
Document
Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure

Authors: Lawrence Dunn, Val Tannen, and Steve Zdancewic

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)


Abstract
Verifying the metatheory of a formal system in Coq involves a lot of tedious "infrastructural" reasoning about variable binders. We present Tealeaves, a generic framework for first-order representations of variable binding that can be used to develop this sort of infrastructure once and for all. Given a particular strategy for representing binders concretely, such as locally nameless or de Bruijn indices, Tealeaves allows developers to implement modules of generic infrastructure called backends that end users can simply instantiate to their own syntax. Our framework rests on a novel abstraction of first-order abstract syntax called a decorated traversable monad (DTM) whose equational theory provides reasoning principles that replace tedious induction on terms. To evaluate Tealeaves, we have implemented a multisorted locally nameless backend providing generic versions of the lemmas generated by LNgen. We discuss case studies where we instantiate this generic infrastructure to simply-typed and polymorphic lambda calculi, comparing our approach to other utilities.

Cite as

Lawrence Dunn, Val Tannen, and Steve Zdancewic. Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{dunn_et_al:LIPIcs.ITP.2023.14,
  author =	{Dunn, Lawrence and Tannen, Val and Zdancewic, Steve},
  title =	{{Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{14:1--14:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.14},
  URN =		{urn:nbn:de:0030-drops-183891},
  doi =		{10.4230/LIPIcs.ITP.2023.14},
  annote =	{Keywords: Coq, category theory, formal metatheory, raw syntax, locally nameless}
}
  • Refine by Author
  • 6 Tannen, Val
  • 4 Deutsch, Alin
  • 2 Amarilli, Antoine
  • 2 Assadi, Sepehr
  • 2 Christophides, Vassilis
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Data provenance
  • 3 Theory of computation → Finite Model Theory
  • 2 Information systems
  • 2 Theory of computation → Type theory
  • 1 Computing methodologies → Anomaly detection
  • Show More...

  • Refine by Keyword
  • 3 provenance
  • 1 Absorptive Semirings
  • 1 Annotation
  • 1 Anomaly Explanation
  • 1 Anomaly Interpretation
  • Show More...

  • Refine by Type
  • 19 document
  • 1 volume

  • Refine by Publication Year
  • 14 2024
  • 1 2005
  • 1 2015
  • 1 2016
  • 1 2017
  • Show More...

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