Tannen, Val
Email Address
ORCID
Disciplines
relationships.isProjectOf
relationships.isOrgUnitOf
Position
Introduction
Research Interests
Collection
50 results
Search Results
Now showing 1 - 10 of 50
Publication Physical Data Independence, Constraints and Optimization with Universal Plans(1999-09-07) Deutsch, Alin; Popa, Lucian; Tannen, ValWe present an optimization method and al gorithm designed for three objectives: physi cal data independence, semantic optimization, and generalized tableau minimization. The method relies on generalized forms of chase and "backchase" with constraints (dependen cies). By using dictionaries (finite functions) in physical schemas we can capture with con straints useful access structures such as indexes, materialized views, source capabilities, access support relations, gmaps, etc. The search space for query plans is defined and enumerated in a novel manner: the chase phase rewrites the original query into a "universal" plan that integrates all the access structures and alternative pathways that are allowed by appli cable constraints. Then, the backchase phase produces optimal plans by eliminating various combinations of redundancies, again according to constraints. This method is applicable (sound) to a large class of queries, physical access structures, and semantic constraints. We prove that it is in fact complete for "path-conjunctive" queries and views with complex objects, classes and dictio naries, going beyond previous theoretical work on processing queries using materialized views.Publication Resource Sharing Through Query Process Migration(2001-01-01) Sahuguet, Arnaud; Tannen, ValIn this paper we focus on systems whose goal is the distribution or exchange of resources such as software packages, scientific data, or multimedia files. To accomplish this goal efficiently, distributed systems find and retrieve resources using combinations of techniques such as brokering, proxying, caching, publish/subscribe, advertising, chaining, referral, recruiting, etc. The resulting architectures are complex and scale with difficulty. We propose two ideas that combine to make such systems much more scalable. One is to encapsulate queries into processes and to use process migration as the basic primitive for cooperation between sites. With this, a generic installer can run at each site, implementing any and all of the techniques mentioned above. The other idea is to describe resource access as "delayed" queries embedded in metadata. Standard distributed database techniques can be applied to the metadata with the additional side-effect of spawning appropriate query processes. We describe a distributed query language that can be obtained by adding our process manipulation primitives to any query language. We discuss installation strategies and we present an algorithm for the site-generic installer on which such a language is based. We also show how to apply query rewriting techniques that allow the installer to perform optimizations. Moreover, we give algorithms that insure that the global amount of installation associated with a given resource retrieval task is bounded.Publication Update Exchange With Mappings and Provenance(2007-11-27) Green, Todd J; Karvounarakis, Grigoris; Ives, Zachary G; Tannen, ValWe consider systems for data sharing among heterogeneous peers related by a network of schema mappings. Each peer has a locally controlled and edited database instance, but wants to ask queries over related data from other peers as well. To achieve this, every peer’s updates propagate along the mappings to the other peers. However, this update exchange is filtered by trust conditions — expressing what data and sources a peer judges to be authoritative — which may cause a peer to reject another’s updates. In order to support such filtering, updates carry provenance information. These systems target scientific data sharing applications, and their general principles and architecture have been described in [21]. In this paper we present methods for realizing such systems. Specifically, we extend techniques from data integration, data exchange, and incremental view maintenance to propagate updates along mappings; we integrate a novel model for tracking data provenance, such that curators may filter updates based on trust conditions over this provenance; we discuss strategies for implementing our techniques in conjunction with an RDBMS; and we experimentally demonstrate the viability of our techniques in the Orchestra prototype system. This technical report supersedes the version which appeared in VLDB 2007 [17] and corrects certain technical claims regarding the semantics of our system (see errata in Sections [3.1] and [4.1.1]).Publication Inheritance as Implicit Coercion(1991-02-01) Tannen, Val; Coquand, Thierry; Gunter, Carl A.; Scedrov, AndreWe present a method for providing semantic interpretations for languages with a type system featuring inheritance polymorphism. Our approach is illustrated on an extension of the language Fun of Cardelli and Wegner, which we interpret via a translation into an extended polymorphic lambda calculus. Our goal is to interpret inheritances in Fun via coercion functions which are definable in the target of the translation. Existing techniques in the theory of semantic domains can be then used to interpret the extended polymorphic lambda calculus, thus providing many models for the original language. This technique makes it possible to model a rich type discipline which includes parametric polymorphism and recursive types as well as inheritance. A central difficulty in providing interpretations for explicit type disciplines featuring inheritance in the sense discussed in this paper arises from the fact that programs can type-check in more than one way. Since interpretations follow the type-checking derivations, coherence theorems are required: that is, one must prove that the meaning of a program does not depend on the way it was type-checked. The proof of such theorems for our proposed interpretation are the basic technical results of this paper. Interestingly, proving coherence in the presence of recursive types, variants, and abstract types forced us to reexamine fundamental equational properties that arise in proof theory (in the form of commutative reductions) and domain theory (in the form of strict vs. non-strict functions).Publication Extensional Models for Polymorphism(1988-04-08) Tannen, Val; Coquand, ThierryWe present a general method for constructing extensional models for the Girard-Reynolds polymorphic lambda calculus - the polymorphic extensional collapse. The method yields models that satisfy additional, computationally motivated constraints like having only two polymorphic booleans and having only the numerals as polymorphic integers. Moreover, the method can be used to show that any simply typed lambda model can be fully and faithfully embedded into a model of the polymorphic lambda calculus.Publication Logical and Computational Aspects of Programming With Sets/Bags/Lists(1991-10-01) Tannen, Val; Subrahmanyam, RameshWe study issues that arise in programming with primitive recursion over non-free datatypes such as lists, bags and sets. Programs written in this style can lack a meaning in the sense that their outputs may be sensitive to the choice of input expression. We are, thus, naturally led to a set-theoretic denotational semantics with partial functions. We set up a logic for reasoning about the definedness of terms and a deterministic and terminating evaluator. The logic is shown to be sound in the model, and its recursion free fragment is shown to be complete for proving definedness of recursion free programs. The logic is then shown to be as strong as the evaluator, and this implies that the evaluator is compatible with the provable equivalence between different set (or bag, or list) expressions. Oftentimes, the same non-free datatype may have different presentations, and it is not clear a priori whether programming and reasoning with the two presentations are equivalent. We formulate these questions, precisely, in the context of alternative presentations of the list, bag, and set datatypes and study some aspects of these questions. In particular, we establish back-and-forth translations between the two presentations, from which it follows that they are equally expressive, and prove results relating proofs of program properties, in the two presentations.Publication Provenance in ORCHESTRA(2010-01-01) Green, Todd J; Ives, Zachary G; Karvounarakis, Grigoris; Tannen, ValSharing structured data today requires agreeing on a standard schema, then mapping and cleaning all of the data to achieve a single queriable mediated instance. However, for settings in which structured data is collaboratively authored by a large community, such as in the sciences, there is seldom con- sensus about how the data should be represented, what is correct, and which sources are authoritative. Moreover, such data is dynamic: it is frequently updated, cleaned, and annotated. The ORCHESTRA collaborative data sharing system develops a new architecture and consistency model for such settings, based on the needs of data sharing in the life sciences. A key aspect of ORCHESTRA’s design is that the provenance of data is recorded at every step. In this paper we describe ORCHESTRA’s provenance model and architecture, emphasizing its integral use of provenance in enforcing trust policies and translating updates efficiently.Publication Putting Lipstick on Pig: Enabling Database-Style Workflow Provenance(2011-12-01) Davidson, Susan B; Amsterdamer, Yael; Stoyanovich, Julia; Tannen, Val; Deutch, DanielWorkflow provenance typically assumes that each module is a “black-box”, so that each output depends on all inputs (coarse-grained dependencies). Furthermore, it does not model the internal state of a module, which can change between repeated executions. In practice, however, an output may depend on only a small subset of the inputs (finegrained dependencies) as well as on the internal state of the module. We present a novel provenance framework that marries database-style and workflow-style provenance, by using Pig Latin to expose the functionality of modules, thus capturing internal state and fine-grained dependencies. A critical ingredient in our solution is the use of a novel form of provenance graph that models module invocations and yields a compact representation of fine-grained workflow provenance. It also enables a number of novel graph transformation operations, allowing to choose the desired level of granularity in provenance querying (ZoomIn and ZoomOut), and supporting “what-if” workflow analytic queries. We implemented our approach in the Lipstick system and developed a benchmark in support of a systematic performance evaluation. Our results demonstrate the feasibility of tracking and querying fine-grained workflow provenance.Publication Optimization Properties for Classes of Conjunctive Regular Path Queries(2001-01-01) Deutsch, Alin; Tannen, ValWe are interested in the theoretical foundations of the optimization of conjunctive regular path queries (CRPQs). The basic problem here is deciding query containment both in the absence and presence of constraints. Containment without constraints for CRPQs is EXPSPACE-complete, as opposed to only NP-complete for relational conjunctive queries. Our past experience with implementing similar algorithms suggests that staying in PSPACE might still be useful. Therefore we investigate the complexity of containment for a hierarchy of fragments of the CRPQ language. The classifying principle of the fragments is the expressivity of the regular path expressions allowed in the query atoms. For most of these fragments, we give matching lower and upper bounds for containment in the absence of constraints. We also introduce for every fragment a naturally corresponding class of constraints in whose presence we show both decidability and undecidability results for containment in various fragments. Finally, we apply our results to give a complete algorithm for rewriting with views in the presence of constraints for a fragment that contains Kleene-star and disjunction.Publication HOLON/CADSE: Integrating Open Software Standards and Formal Methods to Generate Guideline-Based Decision Support Agents(1999) Silverman, Barry G; Wong, Alex; Lang, Lance; Tannen, Val; Khoury, Allan; Campbell, Keith; Sahuguet, Arnaud; Qiang, ChenThis paper describes the efforts of a consortium that is trying to develop and validate formal methods and a meta-environment for authoring, checking, and maintaining a large repository of machine executable practice guidelines. The goal is to integrate and extend a number of open software standards so that guidelines in the meta-environment become a resource that any vendor can plug their applications into and run in their proprietary environment provided they conform to the interface standards.