[1] 
Salman Saghafi, Ryan Danas, and Daniel J. Dougherty.
Exploring theories with a modelfinding assistant.
In Amy P. Felty and Aart Middeldorp, editors, Automated
Deduction  CADE25  25th International Conference on Automated Deduction,
Berlin, Germany, August 17, 2015, Proceedings, volume 9195 of Lecture
Notes in Computer Science, pages 434449. Springer, 2015.
[ bib 
DOI 
.pdf ]
We present an approach to understanding firstorder theories by exploring their models. A typical use case is the analysis of artifacts such as policies, protocols, configurations, and software designs. For the analyses we offer, users are not required to frame formal properties or construct derivations. Rather, they can explore examples of their designs, confirming the expected instances and perhaps recognizing bugs inherent in surprising instances. Key foundational ideas include: the information preorder on models given by homomorphism, an inductivelydefined refinement of the Herbrand base of a theory, and a notion of provenance for elements and facts in models. The implementation makes use of SMTsolving and an algorithm for minimization with respect to the information preorder on models. Our approach is embodied in a tool, Razor, that is complete for finite satisfiability and provides a readevalprint loop used to navigate the set of finite models of a theory and to display provenance.

[2] 
Daniel J. Dougherty and Joshua D. Guttman.
Decidability for lightweight DiffieHellman protocols.
In IEEE 27th Computer Security Foundations Symposium, CSF
2014, Vienna, Austria, 1922 July, 2014, pages 217231, 2014.
[ bib 
.pdf ]
Many protocols use DiffieHellman key agreement, combined with certified longterm values or digital signatures for authentication. These protocols aim at security goals such as key secrecy, forward secrecy, resistance to key compromise attacks, and various flavors of authentication. However, these protocols are challenging to analyze, both in computational and symbolic models. An obstacle in the symbolic model is the undecidability of unification in many theories in the signature of rings. In this paper, we develop an algebraic version of the symbolic approach, working directly within finite fields, the natural structures for the protocols. The adversary, in giving an attack on a protocol goal in a finite field, may rely on any identity in that field. He defeats the protocol if there are attacks in infinitely many finite fields. We prove that, even for this strong adversary, security goals for a wide class of protocols are decidable.

[3] 
Salman Saghafi and Daniel J. Dougherty.
Razor: Provenance and exploration in modelfinding.
In 4th Workshop on Practical Aspects of Automated Reasoning
(PAAR), 2014.
[ bib 
.pdf ]
Razor is a modelfinder for firstorder theories presented geometric form; geometric logic is a variant of firstorder logic that focuses on "observable" properties. An important guiding principle of Razor is that it be accessible to users who are not necessarily expert in formal methods; application areas include software design, analysis of security protocols and policies, and configuration management. A core functionality of the tool is that it supports exploration of the space of models of a given input theory, as well as presentation of provenance information about the elements and facts of a model. The crucial mathematical tool is the ordering relation on models determined by homomorphism, and Razor prefers models that are minimal with respect to this homomorphismordering.

[4] 
John D. Ramsdell, Daniel J. Dougherty, Joshua D. Guttman, and Paul D. Rowe.
A hybrid analysis for security protocols with state.
In Joint Workshop on Foundations of Computer Security and Formal
and Computational Cryptography (FCS/FCC), 2014.
[ bib 
.pdf ]
Cryptographic protocols rely on messagepassing to coordinate activity among principals. Each principal maintains local state in individual local sessions only as needed to complete that session. However, in some protocols a principal also uses state to coordinate its different local sessions. Sometimes the nonlocal, mutable state is used as a means, for example with smart cards or Trusted Platform Modules. Sometimes it is the purpose of running the protocol, for example in commercial transactions. Many richly developed tools and techniques, based on wellunderstood foundations, are available for design and analysis of pure messagepassing protocols. But the presence of crosssession state poses difficulties for these techniques. In this paper we provide a framework for modeling stateful protocols. We define a hybrid analysis method. It leverages theoremprovingin this instance, the PVS proverfor reasoning about computations over state. It combines that with an “enrichbyneed” approachembodied by CPSAthat focuses on the messagepassing part. As a case study we give a full analysis of the Envelope Protocol, due to Mark Ryan.

[5] 
Tim Nelson, Arjun Guha, Daniel J. Dougherty, Kathi Fisler, and Shriram
Krishnamurthi.
A balance of power: Expressive, analyzable controller programming.
In ACM SIGCOMM Workshop on Workshop on Hot Topics in Software
Defined Networks, 2013.
[ bib 
.pdf ]
Configuration languages for traditional network hardware are often fairly limited and hence easy to analyze. Programmable controllers for softwaredefined networks are far more flexible, but this flexibility results in more opportunities for misconfiguration and greatly complicates analyses. We propose a new networkprogramming paradigm that strikes a balance between expressive power and analysis, providing a highly analyzable core language while allowing the reuse of preexisting code written in more complex production languages. As the first step we have created FlowLog, a declarative language for programming SDN controllers. We show that FlowLog is expressive enough to build some real controller programs. It is also a finitestate language, and thus amenable to many types of analysis, such as modelchecking. In this paper we present FlowLog, show examples of controller programs, and discuss analyzing them.

[6] 
Tim Nelson, Salman Saghafi, Daniel J. Dougherty, Kathi Fisler, and Shriram
Krishnamurthi.
Aluminum: Principled scenario exploration through minimality.
In 35th International Conference on Software Engineering
(ICSE), pages 232241, 2013.
[ bib 
.pdf ]
Scenariofinding tools such as Alloy are widely used to understand the consequences of specifications, with applications to software modeling, security analysis, and verification. This paper focuses on the exploration of scenarios: which scenarios are presented first, and how to traverse them in a welldefined way. We present Aluminum, a modification of Alloy that presents only minimal scenarios: those that contain no more than is necessary. Aluminum lets users explore the scenario space by adding to scenarios and backtracking. It also provides the ability to find what can consistently be used to extend each scenario. We describe the semantic basis of Aluminum in terms of minimal models of firstorder logic formulas. We show how this theory can be implemented atop existing SATsolvers and quantify both the benefits of minimality and its small computational overhead. Finally, we offer some qualitative observations about scenario exploration in Aluminum.

[7] 
Daniel J. Dougherty and Joshua D. Guttman.
An algebra for symbolic DiffieHellman protocol analysis.
In Proceedings of the 7th International Symposium on Trustworthy
Global Computing, 2012.
[ bib 
.pdf ]
We study the algebra underlying symbolic protocol analysis for protocols using DiffieHellman operations. DiffieHellman operations act on a cyclic group of prime order, together with an exponentiation operator. The exponents form a finite field: this rich algebraic structure has resisted previous symbolic approaches. We define an algebra that validates precisely the equations that hold almost always as the order of the cyclic group varies. We realize this algebra as the set of normal forms of a particular rewriting theory. The normal forms allow us to define our crucial notion of indicator, a vector of integers that summarizes how many times each secret exponent appears in a message. We prove that the adversary can never construct a message with a new indicator in our adversary model. Using this invariant, we prove the main security goals achieved by UM, a protocol using DiffieHellman for implicit authentication.

[8] 
Daniel J. Dougherty and Joshua D. Guttman.
Symbolic protocol analysis for DiffieHellman.
CoRR, abs/1202.2168, 2012.
[ bib 
.pdf ]
We extend symbolic protocol analysis to apply to protocols using DiffieHellman operations. DiffieHellman operations act on a cyclic group of prime order, together with an exponentiation operator. The exponents form a finite field. This rich algebraic structure has resisted previous symbolic approaches. We work in an algebra defined by the normal forms of a rewriting theory (modulo associativity and commutativity). These normal forms allow us to define our crucial notion of indicator, a vector of integers that summarizes how many times each secret exponent appears in a message. We prove that the adversary can never construct a message with a new indicator in our adversary model. Using this invariant, we prove the main security goals achieved by several different protocols that use DiffieHellman operators in subtle ways. We also give a modeltheoretic justification of our rewriting theory: the theory proves all equations that are uniformly true as the order of the cyclic group varies.

[9] 
Timothy Nelson, Daniel J. Dougherty, Kathi Fisler, and Shriram Krishnamurthi.
Toward a more complete Alloy.
In Abstract State Machines, Alloy, B, VDM, and Z  Third
International Conference, ABZ 2012, Pisa, Italy, June 1821, 2012.
Proceedings, volume 7316 of Lecture Notes in Computer Science, pages
136149. Springer, 2012.
[ bib 
.pdf ]
Many modelfinding tools, such as Alloy, charge users with providing bounds on the sizes of models. It would be preferable to automatically compute sufficient upperbounds whenever possible. The BernaysSchönfinkelRamsey fragment of firstorder logic can relieve users of this burden in some cases: its sentences are satisfiable iff they are satisfied in a finite model, whose size is computable from the input problem. Researchers have observed, however, that the class of sentences for which such a theorem holds is richer in a manysorted frameworkwhich Alloy inhabitsthan in the onesorted case. This paper studies this phenomenon in the general setting of ordersorted logic supporting overloading and empty sorts. We establish a syntactic condition generalizing the BernaysSchönfinkelRamsey form that ensures the Finite Model Property. We give a lineartime algorithm for deciding this condition and a polynomialtime algorithm for computing the bound on model sizes. As a consequence, modelfinding is a complete decision procedure for sentences in this class. Our work has been incorporated into Margrave, a tool for policy analysis, and applies in realworld situations.

[10] 
Mo Liu, Medhabi Ray, Dazhi Zhang, Elke A. Rundensteiner, Daniel J. Dougherty,
Chetan Gupta, Song Wang, and Ismail Ari.
Realtime healthcare services via nested complex event processing
technology.
In 15th International Conference on Extending Database
Technology, EDBT '12, Berlin, Germany, March 2730, 2012, Proceedings, pages
622625, 2012.
[ bib ]
Complex Event Processing (CEP) over event streams has become increasingly important for realtime applications ranging from healthcare to supply chain management. In such applications, arbitrarily complex sequence patterns as well as non existence of such complex situations must be detected in real time. To assure realtime responsiveness for detection of such complex pattern over high volume highspeed streams, efficient processing techniques must be designed. Unfortunately the efficient processing of complex sequence queries with negations remains a largely open problem to date. To tackle this shortcoming, we designed optimized strategies for handling nested CEP query. In this demonstration, we propose to showcase these techniques for processing and optimizing nested pattern queries on streams. In particular our demonstration showcases a platform for specifying complex nested queries, and selecting one of the alternative optimized techniques including subexpression sharing and intermediate result caching to process them. We demonstrate the efficiency of our optimized strategies by graphically comparing the execution time of the optimized solution against that of the default processing strategy of nested CEP queries. We also demonstrate the usage of the proposed technology in several healthcare services.

[11] 
Mo Liu, Elke A. Rundensteiner, Daniel J. Dougherty, Chetan Gupta, Song Wang,
Ismail Ari, and Abhay Mehta.
Highperformance nested CEP query processing over event streams.
In Proceedings of the 27th International Conference on Data
Engineering, ICDE 2011, April 1116, 2011, Hannover, Germany, pages
123134, 2011.
[ bib 
.pdf ]
Complex event processing (CEP) over event streams has become increasingly important for realtime applications ranging from health care, supply chain management to business intelligence. These monitoring applications submit complex queries to track sequences of events that match a given pattern. As these systems mature the need for increasingly complex nested sequence query support arises, while the stateofart CEP systems mostly support the execution of flat sequence queries only. To assure realtime responsiveness and scalability for pattern detection even on huge volume highspeed streams, efficient processing techniques must be designed. In this paper, we first analyze the prevailing nested pattern query processing strategy and identify several serious shortcomings. Not only are substantial subsequences first constructed just to be subsequently discarded, but also opportunities for shared execution of nested subexpressions are overlooked. As foundation, we introduce NEEL, a CEP query language for expressing nested CEP pattern queries composed of sequence, negation, AND and OR operators. To overcome deficiencies, we design rewriting rules for pushing negation into inner subexpressions. Next, we devise a normalization procedure that employs these rules for flattening a nested complex event expression. To conserve CPU and memory consumption, we propose several strategies for efficient shared processing of groups of normalized NEEL subexpressions. These strategies include prefix caching, suffix clustering and customized "bitmarking" execution strategies. We design an optimizer to partition the set of all CEP subexpressions in a NEEL normal form into groups, each of which can then be mapped to one of our shared execution operators. Lastly, we evaluate our technologies by conducting a performance study to assess the CPU processing time using realworld stock trades data. Our results confirm that our NEEL execution in many cases performs 100 fold faster than the traditional iterative nested execution strategy for real stock market query workloads.

[12] 
Medhabi Ray, Mo Liu, Elke A. Rundensteiner, Daniel J. Dougherty, Chetan Gupta,
Song Wang, Abhay Mehta, and Ismail Ari.
Optimizing complex sequence pattern extraction using caching.
In Serge Abiteboul, Klemens Böhm, Christoph Koch, and KianLee
Tan, editors, Workshops Proceedings of the 27th International Conference
on Data Engineering, ICDE 2011, April 1116, 2011, Hannover, Germany, pages
243248, 2011.
[ bib 
.pdf ]
Complex Event Processing (CEP) has become increasingly important for tracking and monitoring complex event anomalies and trends in event streams emitted from business processes such as supply chain management to online stores in ecommerce. These monitoring applications submit complex event queries to track sequences of events that match a given pattern. The stateoftheart CEP systems mostly focus on the execution of flat sequence queries, we instead support the execution of nested CEP queries specified by our NEsted Event Language NEEL. However, the iterative execution of nested CEP expressions often results in the repeated recomputation of the same or similar results for nested subexpressions as the window slides over the event stream. In this work we thus propose to optimize NEEL execution performance by caching intermediate results. In particular we design two methods of applying selective caching of intermediate results namely Object Caching and the IntervalDriven Semantic Caching. Techniques for incrementally loading, purging and exploiting the cache content are described. Our experimental study using realworld stock trades evaluates the performance of our proposed caching strategies for different query types.

[13] 
Timothy Nelson, Christopher Barratt, Daniel J. Dougherty, Kathi Fisler, and
Shriram Krishnamurthi.
The Margrave tool for firewall analysis.
In Proceedings of the 24th USENIX Large Installation System
Administration Conference (LISA 2010), 2010.
[ bib 
.pdf ]
Writing and maintaining firewall configurations can be challenging, even for experienced system administrators. Tools that uncover the consequences of configurations and edits to them can help sysadmins prevent subtle yet serious errors. Our tool, Margrave, offers powerful features for firewall analysis, including enumerating consequences of configuration edits, detecting overlaps and conflicts among rules, tracing firewall behavior to specific rules, and verification against security goals. Margrave differs from other firewallanalysis tools in supporting queries at multiple levels (rules, filters, firewalls, and networks of firewalls), comparing separate firewalls in a single query, supporting reflexive ALCs, and presenting exhaustive sets of concrete scenarios that embody queries. Margrave supports realworld firewallconfiguration languages, decomposing them into multiple policies that capture different aspects of firewall functionality. We present evaluation on networkingforum posts and on an inuse enterprise firewallconfiguration.

[14] 
Daniel J./ Dougherty and Luigi Liquori.
Logic and computation in a lambda calculus with intersection and
union types.
In Proc. 16th International Conference on Logic for Programming
Artificial Intelligence and Reasoning (LPAR), 2010.
[ bib 
.pdf ]
We present an explicitly typed lambda calculus “a la Church” based on the union and intersection types discipline; this system is the counterpart of the standard type assignment calculus “a la Curry.” Our typed calculus enjoys Subject Reduction and confluence, and typed terms are strongly normalizing when the universal type is omitted. Moreover both type checking and type reconstruction are decidable. In contrast to other typed calculi, a system with union types will fail to be “coherent” in the sense of Tannen, Coquand, Gunter, and Scedrov: different proofs of the same typing judgment will not necessarily have the same meaning. In response, we introduce a decidable notion of equality on typeassignment derivations inspired by the equational theory of bicartesianclosed categories.

[15] 
Timothy Nelson, Daniel J. Dougherty, Kathi Fisler, and Shriram Krishnamurthi.
On the finite model property in ordersorted logic.
Technical report, Worcester Polytechnic Institute, 2010.
[ bib 
.pdf ]
The SchoenfinkelBernaysRamsey class is a fragment of firstorder logic with the Finite Model Property: a sentence in this class is satisfiable if and only if it is satisfied in a finite model. Since an upper bound on the size of such a model is computable from the sentence, the satisfiability problem for this family is decidable. Sentences in this form arise naturally in a variety of application areas, and several popular reasoning tools explicitly target this class. Others have observed that the class of sentences for which such a finite model theorem holds is richer in a manysorted framework than in the onesorted case. This paper makes a systematic study of this phenomenon in the general setting of ordersorted logic supporting overloading and empty sorts. We establish a syntactic condition generalizing the SchoenfinkelBernaysRamsey form that ensures the Finite Model Property. We give a lineartime algorithm for deciding this condition and a polynomialtime algorithm for computing the bound on model sizes. As a consequence, modelfinding is a complete decision procedure for sentences in this class. Our algorithms have been incorporated into Margrave, a tool for analysis of accesscontrol and firewall policies, and are available in a standalone application suitable for analyzing input to the Alloy model finder.

[16] 
Kathi Fisler, Shriram Krishnamurthi, and Daniel J. Dougherty.
Embracing policy engineering.
In Proceedings of the Workshop on Future of Software Engineering
Research, FoSER 2010, at the 18th ACM SIGSOFT International Symposium on
Foundations of Software Engineering, 2010, Santa Fe, NM, USA, November 711,
2010, pages 109110, 2010.
[ bib 
.pdf ]
Declarative policies play a central role in many modern software systems. Engineering policies and their interactions with programs raises many interesting open questions.

[17] 
Mo Liu, Medhabi Ray, Elke A. Rundensteiner, Daniel J. Dougherty, Chetan Gupta,
Song Wang, Ismail Ari, and Abhay Mehta.
Processing nested complex sequence pattern queries over event
streams.
In Proceedings of the 7th Workshop on Data Management for Sensor
Networks, in conjunction with VLDB, DMSN 2010, Singapore, September 13,
2010, pages 1419, 2010.
[ bib 
.pdf ]
Complex event processing (CEP) has become increasingly important for tracking and monitoring applications ranging from health care, supply chain management to surveillance. These monitoring applications submit complex event queries to track sequences of events that match a given pattern. As these systems mature the need for increasingly complex nested sequence queries arises, while the stateoftheart CEP systems mostly focus on the execution of flat sequence queries only. In this paper, we now introduce an iterative execution strategy for nested CEP queries composed of sequence, negation, AND and OR operators. Lastly we have introduced the promising direction of applying selective caching of intermediate results to optimize the execution. Our experimental study using realworld stock trades evaluates the performance of our proposed iterative execution strategy for different query types.

[18] 
Tony Bourdier, Horatiu Cirstea, Daniel J. Dougherty, and Hélène
Kirchner.
Extensional and intensional strategies.
In Maribel Fernández, editor, Proceedings Ninth
International Workshop on Reduction Strategies in Rewriting and Programming,
volume 15 of EPTCS, pages 119, 2009.
[ bib 
.pdf ]
This paper is a contribution to the theoretical foundations of strategies. We first present a general definition of abstract strategies which is extensional in the sense that a strategy is defined explicitly as a set of derivations of an abstract reduction system. We then move to a more intensional definition supporting the abstract view but more operational in the sense that it describes a means for determin ing such a set. We characterize the class of extensional strategies that can be defined intensionally. We also give some hints towards a logical characterization of intensional strategies and propose a few challenging perspectives.

[19] 
Venkatesh Raghavan, Yali Zhu, Elke A. Rundensteiner, and Daniel J. Dougherty.
Multijoin continuous query optimization: Covering the spectrum of
linear, acyclic, and cyclic queries.
In Dataspace: The Final Frontier, 26th British National
Conference on Databases, BNCOD 26, Birmingham, UK, July 79, 2009.
Proceedings, volume 5588 of Lecture Notes in Computer Science, pages
91106, 2009.
[ bib 
.pdf ]
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 polynomialtime 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 stateoftheart algorithms. This study has revealed that heuristicbased techniques tend to generate substandard 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 NPcomplete, we present an algorithm FAB which improves other heuristicbased techniques by (i) increasing the likelihood of finding an optimal plan and (ii) improving the effectiveness of finding a nearoptimal 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 QAware approach that selects the optimization algorithm used for generating the join order, based on the shape of the query.

[20] 
Daniel J. Dougherty.
An improved algorithm for generating database transactions from
relational algebra specifications.
In Proc. 10th International Workshop on RuleBased Programming
(RULE), 2009.
[ bib 
.pdf ]
Alloy is a lightweight modeling formalism based on relational algebra. In prior work with Fisler, Giannakopoulos, Krishnamurthi, and Yoo, we have presented a tool, Alchemy, that compiles Alloy specifications into implementations that execute against persistent databases. The foundation of Alchemy is an algorithm for rewriting relational algebra formulas into code for database transactions. In this paper we report on recent progress in improving the robustness and efficiency of this transformation.

[21] 
Theophilos Giannakopoulos, Daniel J. Dougherty, Kathi Fisler, and Shriram
Krishnamurthi.
Towards an operational semantics for Alloy.
In Proc. 16th International Symposium on Formal Methods, pages
483498, 2009.
[ bib 
.pdf ]
The Alloy modeling language has a mathematically rigorous denotational semantics based on relational algebra. Alloy specifications often represent operations on a state, suggesting a transitionsystem semantics. Because Alloy does not intrinsically provide a notion of state, however, this interpretation is only implicit in the relationalalgebra semantics underlying the Alloy Analyzer. In this paper we demonstrate the subtlety of representing state in Alloy specifications. We formalize a natural notion of transition semantics for statebased specifications and show examples of specifications in this class for which analysis based on relational algebra can induce false confidence in designs. We characterize the class of facts that guarantees that Alloy's analysis is sound for statetransition systems, and offer a sufficient syntactic condition for membership in this class. We offer some practical evaluation of the utility of this syntactic discipline and show how it provides a foundation for program synthesis from Alloy.

[22]  Daniel J. Dougherty and Santiago Escobar, editors. Proceedings of the Third International Workshop on Security and Rewriting Techniques (SecReT 2008), volume 234 of Electronic Notes in Theoretical Computer Science, 2009. [ bib ] 
[23] 
Shriram Krishnamurthi, Daniel J. Dougherty, Kathi Fisler, and Daniel Yoo.
Alchemy: Transmuting base Alloy specifications into
implementations.
In ACM SIGSOFT International Symposium on the Foundations of
Software Engineering, pages 158169, 2008.
[ bib 
.pdf ]
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 nontrivial specification. We also discuss lessons learned about the relationship between Alloy specifications and imperative implementations.

[24] 
Daniel J. Dougherty, Silvia Ghilezan, and Pierre Lescanne.
Characterizing strong normalization in the CurienHerbelin
symmetric lambda calculus: extending the CoppoDezani heritage.
Theor. Comput. Sci., 398(13):114128, 2008.
[ bib 
.pdf ]
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 callbyname and callbyvalue. 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.

[25] 
Daniel J. Dougherty, Kathi Fisler, and Shriram Krishnamurthi.
Obligations and their interaction with programs.
In 12th European Symposium On Research In Computer Security
(ESORICS), volume 4734 of Lecture Notes in Computer Science, pages
375389, 2007.
[ bib 
.pdf ]
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.

[26] 
Daniel J. Dougherty, Claude Kirchner, Helene Kirchner, and Anderson Santana
de Oliveira.
Modular access control via strategic rewriting.
In 12th European Symposium On Research In Computer Security
(ESORICS), volume 4734 of Lecture Notes in Computer Science, pages
578593, 2007.
[ bib 
.pdf ]
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. Wellestablished 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.

[27] 
Daniel J. Dougherty.
Core XACML and term rewriting.
Technical Report WPICSTR0707, Worcester Polytechnic Iinstitute,
2007.
[ bib 
.pdf ]
We define a notion of “core” XACML policies and show how these can be represented as ground associativecommutative term rewriting systems with strategies.

[28] 
Daniel J. Dougherty, Silvia Ghilezan, and Pierre Lescanne.
A general technique for analyzing termination in symmetric proof
calculi.
In 9th International Workshop on Termination (WST), 2007.
[ bib 
.pdf ]
Proofterm 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 lambdacalculus of Barbanera and Berardi.

[29] 
Daniel J. Dougherty, Kathi Fisler, and Shriram Krishnamurthi.
Specifying and reasoning about dynamic accesscontrol policies.
In 3rd International Joint Conference on Automated Reasoning
(IJCAR), volume 4130 of Lecture Notes in Computer Science, pages
632646, 2006.
[ bib 
.pdf ]
Accesscontrol policies have grown from simple matrices to nontrivial 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 accesscontrol policies in a dynamic environment. We then specify several interesting, decidable analyses using firstorder temporal logic. Our work illustrates the subtle interplay between logical and statebased methods, particularly in the presence of threevalued policies. We also define a notion of policy equivalence that is especially useful for modular reasoning.

[30] 
Daniel J. Dougherty, Pierre Lescanne, and Luigi Liquori.
Addressed term rewriting systems: Application to a typed object
calculus.
Mathematical Structures in Computer Science, 16:667709, 2006.
[ bib 
.pdf ]
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 objectbased languages, and as an example we present a language incorporating both functional and objectbased 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.

[31] 
Murali Mani, Song Wang, Daniel J. Dougherty, and Elke A. Rundensteiner.
Join minimization in XMLtoSQL translation: An algebraic
approach.
Bulletin of ACM SIGMOD, 35(1), 2006.
[ bib 
.pdf ]
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.

[32] 
Daniel J. Dougherty and Claudio Gutiérrez.
Normal forms and reduction for theories of binary relations.
Theoretical Computer Science, 360(13):228246, 2006.
[ bib 
.pdf ]
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.

[33] 
Daniel J. Dougherty, Silvia Ghilezan, Silvia Likavec, and Pierre Lescanne.
Strong normalization of the dual classical sequent calculus.
In 12th International Conference on Logic for Programming,
Artificial Intelligence and Reasoning (LPAR), 2005.
[ bib 
.pdf ]
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.

[34] 
Daniel J. Dougherty, Pierre Lescanne, Luigi Liquori, and Frederic Lang.
Addressed term rewriting systems: Syntax, semantics, and pragmatics:
Extended abstract.
Electr. Notes Theor. Comput. Sci., 127(5):5782, 2005.
[ bib 
.pdf ]
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 objectbased languages, as for instance the family of languages called λObja, involving both functional and objectbased features.

[35] 
Daniel J. Dougherty, Silvia Ghilezan, and Pierre Lescanne.
Intersection and union types in the λμμ calculus.
Electr. Notes Theor. Comput. Sci., 136:153172, 2005.
[ bib 
.pdf ]
The original λμμ calculus of Curien and Herbelin has a system of simple types, based on sequent calculus, embodying a CurryHoward correspondence with classical logic. We introduce and discuss three type assignment systems that are extensions of lambdamumu with intersection and union types. The intrinsic symmetry in the lambdamumu calculus leads to an essential use of both intersection and union types.

[36] 
Daniel J. Dougherty and Stanley M. Selkow.
The complexity of the certification of properties of stable marriage.
Inf. Process. Lett., 92(6):275277, 2004.
[ bib 
.pdf ]
We give some lower bounds on the certificate complexity of some problems concerning stable marriage, answering a question of Gusfield and Irving.

[37] 
Daniel J. Dougherty, Silvia Ghilezan, and Pierre Lescanne.
Characterizing strong normalization in a language with control
operators.
In 6th ACMSIGPLAN International Conference on Principles and
Practice of Declarative Programming (PPDP), 2004.
[ bib 
.pdf ]
We investigate some fundamental properties of the reduction relation in the untyped term calculus derived from Curien and Herbelin's lambdamumu . The original lambdamumu has a system of simple types, based on sequent calculus, embodying a CurryHoward correspondence with classical logic; the significance of the untyped calculus of raw terms is that it is a Turingcomplete 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 uniontypes systems in the literature, our system enjoys the Subject Reduction property.

[38] 
Daniel J. Dougherty and Carlos Martinez.
Unification and matching modulo type isomorphism.
In 2nd International Workshop on HigherOrder Rewriting, 2004.
[ bib 
.pdf ]
We present some initial results in an investigation of higherorder unification and matching in the presence of type isomorphism

[39] 
Stephane Lengrand, Pierre Lescanne, Daniel J. Dougherty, Mariangiola
DezaniCiancaglini, and Steffen van Bakel.
Intersection types for explicit substitutions.
Information and Computation, 189(1):1742, 2004.
[ bib 
.pdf ]
We present a new system of intersection types for a compositionfree 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.

[40] 
Daniel J. Dougherty and Pierre Lescanne.
Reductions, intersection types, and explicit substitutions.
Mathematical Structures in Computer Science, 13(1):5585,
2003.
[ bib 
.pdf ]
This paper is part of a general programme of treating explicit substitutions as the primary lambdacalculi from the point of view of foundations as well as applications. We work in a compositionfree calculus of explicit substitutions and an augmented calculus obtained by adding explicit garbagecollection, and explore the relationship between intersectiontypes 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 headreduction are nondeterministic, 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 lambdacalculus, which in our view is subordinate to the calculus of explicit substitution.

[41] 
Daniel J. Dougherty, Pierre Lescanne, and Stéphane Lengrand.
An improved system of intersection types for explicit substitutions.
In Proc. Conf. Foundations of Information Technology in the Era
of Network and Mobile Computing, pages 511524. 2nd IFIP International
Conference on Theoretical Computer Science, 2002.
[ bib ]
We characterize those terms which are strongly normalizing in a compositionfree 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.

[42] 
Daniel J. Dougherty and ToMasz Wierzbicki.
A decidable variant of higher order matching.
In Proc. Thirteenth Intl. Conf. on Rewriting Techniques and
Applications (RTA), volume 2378 of Lecture Notes in Computer Science,
pages 340351, 2002.
[ bib 
.pdf ]
A lambda term is kduplicating 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 kduplicating (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 1duplicating) is in NP, generalizing de Groote's result for the linear lambda calculus.

[43] 
Daniel J. Dougherty and Pierre Lescanne.
Reductions, intersection types, and explicit substitutions (extended
abstract).
In S. Abramsky, editor, Proc. 5th Int. Conf. on Typed Lambda
Calculus and Applications (TLCA), volume 2044 of Lecture Notes in
Computer Science, pages 121135, Krakow, Poland, 2001.
[ bib 
.pdf ]

[44] 
F. Lang, P. Lescanne, L. Liquori, Daniel J. Dougherty, and K. Rose.
Obj+a, a generic objectcalculus based on addressed term rewriting
systems with modules.
In WESTAPP 01: The Fourth International Workshop on Explicit
Substitutions: Theory and Applications to Programs and Proofs, 2001.
[ bib ]

[45] 
Daniel J. Dougherty and Claudio Gutiérrez.
Normal forms and reduction for theories of binary relations.
In Proc. Eleventh Intl. Conf. on Rewriting Techniques and
Applications (RTA), volume 1833 of Lecture Notes in Computer Science,
pages 95109, 2000.
[ bib ]

[46] 
Daniel J. Dougherty and Ramesh Subrahmanyam.
Equality between functionals in the presence of coproducts.
Information and Computation, 157(1,2):5283, 2000.
[ bib 
.pdf ]
We consider the lambdacalculus obtained from the simplytyped 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 settheoretic model with an infinite base type.

[47] 
Frederic Lang, Daniel J. Dougherty, Pierre Lescanne, Luigi Liquori, and
Kristoffer Rose.
Addressed term rewriting systems.
Technical Report RR 199930, Ecole Normale Superieure de Lyon, 1999.
[ bib 
.pdf ]
We propose Addressed Term Rewriting Systems (ATRS) as a solution to the stillstanding 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 “backpointer” 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.

[48] 
F. Lang, P. Lescanne, L. Liquori, Daniel J. Dougherty, and K. Rose.
A Generic ObjectCalculus Based on Addressed Term
Rewriting Systems.
Technical Report RR199954, Laboratoire de l'Informatique et du
Parallelisme, ENS Lyon, 1999.
[ bib 
.pdf ]

[49] 
Friedrich Otto, Paliath Narendran, and Daniel J. Dougherty.
Equational unification, word unification, and 2ndorder equational
unification.
Theoretical Computer Science, 198(12):147, 1998.
[ bib 
.pdf ]
For finite convergent termrewriting systems the equational unification problem is shown to be recursively independent of the equational matching problem, the word matching problem, and the (simultaneous) 2ndorder equational matching problem. We also present some new decidability results for simultaneous equational unification and 2ndorder equational matching.

[50] 
Daniel J. Dougherty and Ramesh Subrahmanyam.
Equality between functionals in the presence of coproducts.
In Proc. Tenth Annual IEEE Symposium on Logic in Computer
Science, pages 282291, San Diego, California, 1995. IEEE Computer Society
Press.
[ bib ]

[51] 
Friedrich Otto, Paliath Narendran, and Daniel J. Dougherty.
Some independence results for equational unification.
In Proc. Sixth Intl. Conf. on Rewriting Techniques and
Applications (RTA 1995), volume 914 of Lecture Notes in Computer
Science, pages 367381, 1995.
[ bib ]

[52] 
Daniel J. Dougherty and Patricia Johann.
A combinatory logic approach to higherorder Eunification.
Theoretical Computer Science, 139(12):207242, 1995.
[ bib 
.pdf ]
Let E be a firstorder equational theory. A translation of typed higherorder Eunification 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 higherorder Eunifiers. In fact, we treat a more general problem, in which the types of terms contain type variables.

[53] 
Daniel J. Dougherty.
Some lambda calculi with categorical sums and products.
In Claude Kirchner, editor, Proc. 5th International Conference
on Rewriting Techniques and Applications (RTA), volume 690 of Lecture
Notes in Computer Science, pages 137151, Berlin, 1993. SpringerVerlag.
[ bib 
.pdf ]
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 (basetype) confluence is proved for the full calculus; full confluence is proved for the calculus omitting the rule for strong sums. In the latter case, fixedpoint constructors may be added while retaining confluence.

[54] 
Daniel J. Dougherty.
Closed categories and categorial grammar.
Notre Dame Journal of Formal Logic, 34(1):3649, 1993.
[ bib 
.pdf ]
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 syntaxcategory and a semanticscategory, the fundamental properties of biclosed categories induce a rudimentary computationally oriented theory of language.

[55] 
Daniel J. Dougherty.
Higherorder unification via combinators.
Theoretical Computer Science, 114(2):273298, 1993.
[ bib 
.pdf ]
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 typevariables, so that a solution may involve typesubstitution as well as termsubstitution. 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.

[56] 
Daniel J. Dougherty and Patricia Johann.
A combinatory logic approach to higherorder EUnification.
In Deepak Kapur, editor, Proc. 11th International Conference on
Automated Deduction (CADE11), volume 607 of Lecture Notes in
Artificial Intelligence, pages 7993, Saratoga Springs, NY, 1992.
[ bib ]

[57] 
Daniel J. Dougherty and Patricia Johann.
An improved general Eunification method.
Journal of Symbolic Computation, 14(4):303320, 1992.
[ bib 
.pdf ]
A generalization of Paramodulation is defined and shown to lead to a complete Eunification 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.

[58] 
Daniel J. Dougherty.
Adding algebraic rewriting to the untyped lambda calculus.
Information and Computation, 101(2):251267, 1992.
[ bib 
.pdf ]
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 betareduction plus rewriting; we sketch the application to the polymorphic lambda calculus.

[59] 
Daniel J. Dougherty.
Adding algebraic rewriting to the untyped lambda calculus (extended
abstract).
In Ron Book, editor, Proc. of the Fourth International
Conference on Rewriting Techniques and Applications (Como, Italy), volume
488 of Lecture Notes in Computer Science, pages 3748, 1991.
[ bib ]

[60] 
Daniel J. Dougherty.
A strong Baire category theorem for products.
Topology and Its Applications, 39:105112, 1991.
[ bib ]

[61] 
Daniel J. Dougherty and Patricia Johann.
An improved general Eunification method.
In M. Stickel, editor, Proc. 10th International Conference on
Automated Deduction, Kaiserslautern (Germany), volume 449 of Lecture
Notes in Computer Science, pages 261275, 1990.
[ bib ]

[62] 
Daniel J. Dougherty.
Decomposition of infinite matrices.
Journal of Combinatorial Theory (Series A), 45:277289, 1987.
[ bib ]

[63] 
Daniel J. Dougherty, R. M. Shortt, and R. N. Ball.
Decomposition theorems for measures.
Journal of Mathematical Analysis and Applications,
128:561580, 1987.
[ bib ]

[64] 
Daniel J. Dougherty.
Gentzen systems, resolution, and literal trees.
Notre Dame Journal of Formal Logic, 27:483503, 1986.
[ bib ]

This file was generated by bibtex2html 1.96.