Traditional optimization algorithms that guarantee optimal plans have exponential time complexity and are thus not viable in streaming contexts. Continuous query optimizers commonly adopt heuristic techniques such as Adaptive Greedy to attain polynomial-time execution. However, these techniques are known to produce optimal plans only for linear and star shaped join queries. Motivated by the prevalence of acyclic, cyclic and even complete query shapes in stream applications, we conduct an extensive experimental study of the behavior of the state-of-the-art algorithms. This study has revealed that heuristic-based techniques tend to generate sub-standard plans even for simple acyclic join queries. For general acyclic join queries we extend the classical IK approach to the streaming context to define an algorithm TreeOpt that is guaranteed to find an optimal plan in polynomial time. For the case of cyclic queries, for which finding optimal plans is known to be NP-complete, we present an algorithm FAB which improves other heuristic-based techniques by (i) increasing the likelihood of finding an optimal plan and (ii) improving the effectiveness of finding a near-optimal plan when an optimal plan cannot be found in polynomial time. To handle the entire spectrum of query shapes from acyclic to cyclic we propose a Q-Aware approach that selects the optimization algorithm used for generating the join order, based on the shape of the query.

Alloy specifications are used to define lightweight models of systems. We present Alchemy, which compiles Alloy specifications into implementations that execute against persistent databases. Alchemy translates a subset of Alloy predicates into imperative update operations, and it converts facts into database integrity constraints that it maintains automatically in the face of these imperative actions. In addition to presenting the semantics and an algorithm for this compilation, we present the tool and outline its application to a non-trivial specification. We also discuss lessons learned about the relationship between Alloy specifications and imperative implementations.

We develop an intersection type system for the λ-μ-μ  calculus of Curien and Herbelin. This calculus provides a symmetric computational interpretation of classical sequent style logic and gives a simple account of call-by-name and call-by-value. The present system improves on earlier type disciplines for the calculus: in addition to characterizing the expressions that are strongly normalizing under free (unrestricted) reduction, the system enjoys the Subject Reduction and the Subject Expansion properties.

Obligations are pervasive in modern systems, often linked to access control decisions. We present a very general model of obligations as objects with state, and discuss its interaction with a program's execution. We describe several analyses that the model enables, both static (for verification) and dynamic (for monitoring). This includes a systematic approach to approximating obligations for enforcement. We also discuss some extensions that would enable practical policy notations. Finally, we evaluate the robustness of our model against standard definitions from jurisprudence.

Security policies, in particular access control, are fundamental elements of computer security. We address the problem of authoring and analyzing policies in a modular way using techniques developed in the field of term rewriting, focusing especially on the use of rewriting strategies. Term rewriting supports a formalization of access control with a clear declarative semantics based on equational logic and an operational semantics guided by strategies. Well-established term rewriting techniques allow us to check properties of policies such as the absence of conflicts and the property of always returning a decision. A rich language for expressing rewriting strategies is used to define a theory of modular construction of policies in which we can better understand the preservation of properties of policies under composition. The robustness of the approach is illustrated on the composition operators of XACML.

Proof-term calculi expressing a computational interpretation of classical logic serve as tools for extracting the constructive content of classical proofs and at the same time can be seen as pure programming languages with explicit representation of control. The inherent symmetry in the underlying logic presents technical challenges to the study of the reduction properties of these systems. We explore the use of intersection types for these calculi, note some of the challenges inherent in applying intersection types in a symmetric calculus, and show how to overcome these difficulties. The approach is applicable to a variety of systems under active investigation in the current literature; we apply our techniques in a specific case study: characterizing termination in the symmetric lambda-calculus of Barbanera and Berardi.

We define a notion of “core” XACML and show how these can be represented as ground associative-commutative term rewriting systems with strategies.

Consider an XML view defined over a relational database, and a user query specified over this view. This user XML query is typically processed using the following steps: (a) our translator maps the XML query to one or more SQL queries, (b) the relational engine translates an SQL query to a relational algebra plan, (c) the relational engine executes the algebra plan and returns SQL results, and (d) our translator translates the SQL results back to XML. However, a straightforward approach produces a relational algebra plan after step (b) that is inefficient and has redundant joins. In this paper, we report on our preliminary observations with respect to how joins in such a relational algebra plan can be minimized, while maintaining bag semantics. Our approach works on the relational algebra plan and optimizes it using novel rewrite rules that consider pairs of joins in the plan and determine whether one of them is redundant and hence can be removed. Our study shows that algebraic techniques achieve effective join minimization, and such techniques are useful and can be integrated into mainstream SQL engines.

Access-control policies have grown from simple matrices to non-trivial specifications written in sophisticated languages. The increasing complexity of these policies demands correspondingly strong automated reasoning techniques for understanding and debugging them. The need for these techniques is even more pressing given the rich and dynamic nature of the environments in which these policies evaluate. We define a framework to represent the behavior of access-control policies in a dynamic environment. We then specify several interesting, decidable analyses using first-order temporal logic. Our work illustrates the subtle interplay between logical and state-based methods, particularly in the presence of three-valued policies. We also define a notion of policy equivalence that is especially useful for modular reasoning.

We present a formalism called Addressed Term Rewriting Systems, which can be used to model implementations of theorem proving, symbolic computation, and programming languages, especially aspects of sharing, recursive computations and cyclic data structures. Addressed Term Rewriting Systems are therefore well suited for describing object-based languages, and as an example we present a language incorporating both functional and object-based features. As a case study in how reasoning about languages is supported in the ATRS formalism a type system is defined and a type soundness result is proved.

We consider the representable equational theory of binary relations, in a language expressing composition, converse, and lattice operations. By working directly with a presentation of relation expressions as graphs we are able to define a notion of reduction which is confluent and strongly normalizing and induces a notion of computable normal form for terms. This notion of reduction thus leads to a computational interpretation of the representable theory.

We investigate some syntactic properties of Wadler's dual calculus, a term calculus which corresponds to classical sequent logic in the same way that Parigot's λ-μcalculus corresponds to classical natural deduction. Our main result is strong normalization theorem for reduction in the dual calculus; we also prove some confluence results for the typed and untyped versions of the system.

We present a formalism called Addressed Term Rewriting Systems, which can be used to define the operational semantics of programming languages, especially those involving sharing, recursive computations and cyclic data structures. Addressed Term Rewriting Systems are therefore well suited for describing object-based languages, as for instance the family of languages called λ-Obja, involving both functional and object-based features.

The original λ-μ-μ calculus of Curien and Herbelin has a system of simple types, based on sequent calculus, embodying a Curry-Howard correspondence with classical logic. We introduce and discuss three type assignment systems that are extensions of lambda-mu-mu  with intersection and union types. The intrinsic symmetry in the lambda-mu-mu  calculus leads to an essential use of both intersection and union types.

We give some lower bounds on the certificate complexity of some problems concerning stable marriage, answering a question of Gusfield and Irving.

We investigate some fundamental properties of the reduction relation in the untyped term calculus derived from Curien and Herbelin's lambda-mu-mu . The original lambda-mu-mu  has a system of simple types, based on sequent calculus, embodying a Curry-Howard correspondence with classical logic; the significance of the untyped calculus of raw terms is that it is a Turing-complete language for computation with explicit representation of control as well as code. We define a type assignment system for the raw terms satisfying: a term is typable if and only if it is strongly normalizing. The intrinsic symmetry in the calculus leads to an essential use of both intersection and union types; in contrast to other union-types systems in the literature, our system enjoys the Subject Reduction property.

We present some initial results in an investigation of higher-order unification and matching in the presence of type isomorphism

We present a new system of intersection types for a composition-free calculus of explicit substitutions with a rule for garbage collection, and show that it characterizes those terms which are strongly normalizing. This system extends previous work on the natural generalization of the classical intersection types system, which characterized head normalization and weak normalization, but was not complete for strong normalization. An important role is played by the notion of available variable in a term, which is a generalization of the classical notion of free variable.

This paper is part of a general programme of treating explicit substitutions as the primary lambda-calculi from the point of view of foundations as well as applications. We work in a composition-free calculus of explicit substitutions and an augmented calculus obtained by adding explicit garbage-collection, and explore the relationship between intersection-types and reduction. We show that the terms which normalize by leftmost reduction and the terms which normalize by head reduction can each be characterized as the terms typable in a certain system. The relationship between typability and strong normalization is subtly different from the classical case: we show that typable terms are strongly normalizing but give a counterexample to the converse. Our notions of leftmost- and head-reduction are non-deterministic, and our normalization theorems apply to any computations obeying these strategies. In this way we refine and strengthen the classical normalization theorems. The proofs require some new techniques in the presence of reductions involving explicit substitutions. Indeed, in our proofs we do not rely on results from classical lambda-calculus, which in our view is subordinate to the calculus of explicit substitution.

We characterize those terms which are strongly normalizing in a composition-free calculus of explicit substitutions by defining a suitable type system using intersection types. The key idea is the notion of available variable in a term, which is a generalization of the classical notion of free variable.

A lambda term is k-duplicating if every occurrence of a lambda abstractor binds at most k variable occurrences. We prove that the problem of higher order matching where solutions are required to be k-duplicating (but with no constraints on the problem instance itself) is decidable. We also show that the problem of higher order matching in the affine lambda calculus (where both the problem instance and the solutions are constrained to be 1-duplicating) is in NP, generalizing de Groote's result for the linear lambda calculus.

We consider the lambda-calculus obtained from the simply-typed calculus by adding products, coproducts, and a terminal type. We prove the following theorem: The equations provable in this calculus are precisely those true in any set-theoretic model with an infinite base type.

We propose Addressed Term Rewriting Systems (ATRS) as a solution to the still-standing problem of finding a simple yet formally useful framework that can account for computation with sharing, cycles, and side effects. ATRS are characterised by the combination of three features: they work with terms where structural induction is useful, they use a minimal “back-pointer” representation of cyclic data, and they ensure a bounded complexity of rewrite steps by eliminating implicit pointer redirection. In the paper we develop this and show how it is a very useful compromise between less abstract term graph rewriting and the more abstract equational rewriting.

For finite convergent term-rewriting systems the equational unification problem is shown to be recursively independent of the equational matching problem, the word matching problem, and the (simultaneous) 2nd-order equational matching problem. We also present some new decidability results for simultaneous equational unification and 2nd-order equational matching.

Let E be a first-order equational theory. A translation of typed higher-order E-unification problems into a typed combinatory logic framework is presented and justified. The case in which E admits presentation as a convergent term rewriting system is treated in detail: in this situation, a modification of ordinary narrowing is shown to be a complete method for enumerating higher-order E-unifiers. In fact, we treat a more general problem, in which the types of terms contain type variables.

We present an algorithm for unification in the simply typed lambda calculus which enumerates complete sets of unifiers using a finitely branching search space. In fact, the types of terms may contain type-variables, so that a solution may involve typesubstitution as well as term-substitution. the problem is first translated into the problem of unification with respect to extensional equality in combinatory logic, and the algorithm is defined in terms of transformations on systems of combinatory terms. These transformations are based on a new method (itself based on systems) for deciding extensional equality between typed combinatory logic terms.

We consider the simply typed λ-calculus with primitive recursion operators and types corresponding to categorical products and coproducts. The standard equations corresponding to extensionality and to surjectivity of pairing and its dual are oriented as expansion rules. Strong normalization and ground (base-type) confluence is proved for the full calculus; full confluence is proved for the calculus omitting the rule for strong sums. In the latter case, fixed-point constructors may be added while retaining confluence.

Inspired by Lambek's work on categorial grammar, we examine the proposal that the theory of biclosed monoidal categories can serve as a foundation for a formal theory of natural language. The emphasis throughout is on the derivation of the axioms for these categories from linguistic intuitions. When Montague's principle that there is a homomorphism between syntax and semantics is refined to the principle that meaning is a functor between a syntax-category and a semantics-category, the fundamental properties of biclosed categories induce a rudimentary computationally oriented theory of language.

We investigate the system obtained by adding an algebraic rewriting system R to an untyped lambda calculus in which terms are formed using the function symbols from R as constants. On certain classes of terms, called here stable, we prove that the resulting calculus is confluent if R is confluent, and terminating if R is terminating. The termination result has the corresponding theorems for several typed calculi as corollaries. The proof of the confluence result suggests a general method for proving confluence of typed beta-reduction plus rewriting; we sketch the application to the polymorphic lambda calculus.

A generalization of Paramodulation is defined and shown to lead to a complete E-unification method for arbitrary equational theories E. The method is defined in terms of transformations on systems, building upon and refining results of Gallier and Snyder.