Intersection and Union Types in the (2008)
Daniel J. Dougherty, Silvia Ghilezan, École Normale, Supérieure Lyon
λµ�µ-calculus
A General Technique for Analyzing Termination in Symmetric Proof Calculi (2008)
Daniel J. Dougherty, Silvia Ghilezan, Pierre Lescanne
Abstract. 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...
Join Minimization in XML-to-SQL Translation: An Algebraic Approach (2008)
Murali Mani, Song Wang, Daniel J. Dougherty, Elke A. Rundensteiner
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...
Abstract Normal forms for binary relations (2008)
Daniel J. Dougherty, Claudio Gutiérrez
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...
Obligations and their Interaction with Programs (2008)
Daniel J. Dougherty, Kathi Fisler, Shriram Krishnamurthi
Abstract. 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...
Closed Categories and Categorial Grammar (2007)
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...
Modular Access Control via Strategic Rewriting (2007)
Daniel J. Dougherty, Claude Kirchner, Hélène Kirchner, Anderson Santana De
Abstract. 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...
Modular Access Control via Strategic Rewriting (2007)
Daniel J. Dougherty, Claude Kirchner, Hélène Kirchner, Anderson Santana De
Abstract. 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...
A request collects a bunch of attributes, into sorts we call SubjectQ, ResourceQ, (2007)
Daniel J. Dougherty, Request Subjectq, Resourceq Actionq Environmentq, Subjectq (attid
We define a notion of “core ” XACML and show how these can be represented as ground associativee-commutative term rewriting systems with strategies. 1 Core XACML The first few sections are an...
Modular Access Control via Strategic Rewriting (2007)
Daniel J. Dougherty, Claude Kirchner, Hélène Kirchner, Anderson Santana De
Abstract. 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...
Modular Access Control via Strategic Rewriting (2007)
Daniel J. Dougherty, Claude Kirchner, Hélène Kirchner, Anderson Santana De
Abstract. 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...
Normal forms for binary relations (2006)
Dougherty, Daniel J., Gutiérrez, Claudio
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...
1.1. Addressed Calculi and Semantics of Sharing (2006)
Daniel J. Dougherty, Pierre Lescanne, Luigi Liquori
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...
Specifying and reasoning about dynamic access-control policies (2006)
Daniel J. Dougherty, Kathi Fisler, Shriram Krishnamurthi
Abstract. Access-control policies have grown from simple matrices to non-trivial specifications written in sophisticated languages. The increasing complexity of these policies demands correspondingly...
Specifying and reasoning about dynamic access-control policies (2006)
Daniel J. Dougherty, Kathi Fisler, Shriram Krishnamurthi
Abstract. Access-control policies have grown from simple matrices to non-trivial specifications written in sophisticated languages. The increasing complexity of these policies demands correspondingly...
Equality Between Functionals in the Presence of Coproducts (1995)
Daniel J. Dougherty, Ramesh Subrahmanyam
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...
Some Independence Results for Equational Unification (1995)
Friedrich Otto, Paliath Narendran, Daniel J. Dougherty
. 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...
An Improved General E-Unification Method (1994)
Daniel J. Dougherty, Patricia Johann
This paper considers the problem of E-unification for arbitrary equational theories E, and presents an inference rule approximating Paramodulation and leading to a complete E-unification procedure...
Higher-Order Unification via Combinators (1993)
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...
Some Lambda Calculi With Categorical Sums and Products (1993)
. 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...
A Combinatory Logic Approach to Higher-order E-unification (1992)
Daniel J. Dougherty, Patricia Johann
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...
Adding algebraic rewriting to the untyped lambda calculus (1992)
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...