Related papers: Two for the Price of One: Lifting Separation Logic…
The logic programming paradigm provides the basis for a new intensional view of higher-order notions. This view is realized primarily by employing the terms of a typed lambda calculus as representational devices and by using a richer form…
Lifting theorems are theorems that relate the query complexity of a function $f:\{0,1\}^{n}\to\{0,1\}$ to the communication complexity of the composed function $f \circ g^{n}$, for some "gadget" $g:\{0,1\}^{b}\times\{0,1\}^{b}\to\{0,1\}$.…
Many security- and performance-critical domains, such as cryptography, rely on low-level verification to minimize the trusted computing surface and allow code to be written directly in assembly. However, verifying assembly code against a…
Separation logic adds two connectives to assertion languages: separating conjunction * ("star") and its adjoint, separating implication -* ("magic wand"). Comparatively, separating implication is less widely used. This paper demonstrates…
Authenticated data structures allow untrusted third parties to carry out operations which produce proofs that can be used to verify an operation's output. Such data structures are challenging to develop and implement correctly. This paper…
We apply to logic programming some recently emerging ideas from the field of reduction-based communicating systems, with the aim of giving evidence of the hidden interactions and the coordination mechanisms that rule the operational…
The paper introduces the notion of off-line justification for Answer Set Programming (ASP). Justifications provide a graph-based explanation of the truth value of an atom w.r.t. a given answer set. The paper extends also this notion to…
Subset models provide a new semantics for justifcation logic. The main idea of subset models is that evidence terms are interpreted as sets of possible worlds. A term then justifies a formula if that formula is true in each world of the…
In this extended abstract we provide a unifying framework that can be used to characterize and compare the expressive power of query languages for different data base models. The framework is based upon the new idea of valid partition, that…
We present a concise proof for the supporting hyperplane theorem. We then observe that the proof not only establishes the supporting hyperplane theorem but also extends it to a hyperplane separation theorem for certain non-convex sets. The…
We introduce derivation depth-a computable metric of the reasoning effort needed to answer a query based on a given set of premises. We model information as a two-layered structure linking abstract knowledge with physical carriers, and…
Variable independence and decomposability are algorithmic techniques for simplifying logical formulas by tearing apart connections between free variables. These techniques were originally proposed to speed up query evaluation in constraint…
Modern data analytics pipelines increasingly combine relational queries, graph processing, and tensor computation within a single application, but existing systems remain fragmented across paradigms, execution models, and research…
Dependence logic is a formalism that augments the syntax of first-order logic with dependence atoms asserting that the value of a variable is determined by the values of some other variables, i.e., dependence atoms express functional…
We continue the work on the relations between independence logic and the model-theoretic analysis of independence, generalizing the results of [15] and [16] to the framework of abstract independence relations for an arbitrary AEC. We give a…
The paper is a contribution both to the theoretical foundations and to the actual construction of efficient automatizable proof procedures for non-classical logics. We focus here on the case of finite-valued logics, and exhibit: (i) a…
In relational verification, judicious alignment of computational steps facilitates proof of relations between programs using simple relational assertions. Relational Hoare logics (RHL) provide compositional rules that embody various…
This paper proposes an alternative to standard first-order logic that seeks greater naturalness, generality, and semantic self-containment. The system removes the first-order restriction, avoids type hierarchies, and dispenses with external…
Definite descriptions are expressions of the form "the unique $x$ satisfying property $C$," which allow reference to objects through their distinguishing characteristics. They play a crucial role in ontology and query languages, offering an…
Heap data is potentially unbounded and seemingly arbitrary. As a consequence, unlike stack and static memory, heap memory cannot be abstracted directly in terms of a fixed set of source variable names appearing in the program being…