[1] Daniel J. Dougherty and Joshua D. Guttman. Decidability for lightweight Diffie-Hellman protocols. In IEEE Symposium on Computer Security Foundations., 2014. [ bib | .pdf ]
Many protocols use Diffie-Hellman key agreement, combined with certified long-term 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.

[2] Salman Saghafi and Daniel J. Dougherty. Razor: Provenance and exploration in model-finding. In 4th Workshop on Practical Aspects of Automated Reasoning (PAAR), 2014. [ bib | .pdf ]
Razor is a model-finder for first-order theories presented geometric form; geometric logic is a variant of first-order 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 homomorphism-ordering.

[3] 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 message-passing 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 non-local, 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 well-understood foundations, are available for design and analysis of pure message-passing protocols. But the presence of cross-session 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 theorem-proving-in this instance, the PVS prover-for reasoning about computations over state. It combines that with an “enrich-by-need” approach-embodied by CPSA-that focuses on the message-passing part. As a case study we give a full analysis of the Envelope Protocol, due to Mark Ryan.

[4] 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 software-defined networks are far more flexible, but this flexibility results in more opportunities for mis-configuration and greatly complicates analyses. We propose a new network-programming paradigm that strikes a balance between expressive power and analysis, providing a highly analyzable core language while allowing the re-use of pre-existing 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 finite-state language, and thus amenable to many types of analysis, such as model-checking. In this paper we present FlowLog, show examples of controller programs, and discuss analyzing them.

[5] 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 232-241, 2013. [ bib | .pdf ]
Scenario-finding 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 well-defined 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 first-order logic formulas. We show how this theory can be implemented atop existing SAT-solvers and quantify both the benefits of minimality and its small computational overhead. Finally, we offer some qualitative observations about scenario exploration in Aluminum.

[6] Daniel J. Dougherty and Joshua D. Guttman. An algebra for symbolic Diffie-Hellman 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 Diffie-Hellman operations. Diffie-Hellman 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 Diffie-Hellman for implicit authentication.

[7] Daniel J. Dougherty and Joshua D. Guttman. Symbolic protocol analysis for Diffie-Hellman. CoRR, abs/1202.2168, 2012. [ bib | .pdf ]
We extend symbolic protocol analysis to apply to protocols using Diffie-Hellman operations. Diffie-Hellman 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 Diffie-Hellman operators in subtle ways. We also give a model-theoretic justification of our rewriting theory: the theory proves all equations that are uniformly true as the order of the cyclic group varies.

[8] 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 18-21, 2012. Proceedings, volume 7316 of Lecture Notes in Computer Science, pages 136-149. Springer, 2012. [ bib | .pdf ]
Many model-finding tools, such as Alloy, charge users with providing bounds on the sizes of models. It would be preferable to automatically compute sufficient upper-bounds whenever possible. The Bernays-Schönfinkel-Ramsey fragment of first-order 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 many-sorted framework-which Alloy inhabits-than in the one-sorted case. This paper studies this phenomenon in the general setting of order-sorted logic supporting overloading and empty sorts. We establish a syntactic condition generalizing the Bernays-Schönfinkel-Ramsey form that ensures the Finite Model Property. We give a linear-time algorithm for deciding this condition and a polynomial-time algorithm for computing the bound on model sizes. As a consequence, model-finding 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 real-world situations.

[9] 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 27-30, 2012, Proceedings, pages 622-625, 2012. [ bib ]
Complex Event Processing (CEP) over event streams has become increasingly important for real-time 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 real-time responsiveness for detection of such complex pattern over high volume high-speed 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 sub-expression 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.

[10] Mo Liu, Elke A. Rundensteiner, Daniel J. Dougherty, Chetan Gupta, Song Wang, Ismail Ari, and Abhay Mehta. High-performance nested CEP query processing over event streams. In Proceedings of the 27th International Conference on Data Engineering, ICDE 2011, April 11-16, 2011, Hannover, Germany, pages 123-134, 2011. [ bib | .pdf ]
Complex event processing (CEP) over event streams has become increasingly important for real-time 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 state-of-art CEP systems mostly support the execution of flat sequence queries only. To assure real-time responsiveness and scalability for pattern detection even on huge volume high-speed 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 "bit-marking" 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 real-world 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.

[11] 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 Kian-Lee Tan, editors, Workshops Proceedings of the 27th International Conference on Data Engineering, ICDE 2011, April 11-16, 2011, Hannover, Germany, pages 243-248, 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 e-commerce. These monitoring applications submit complex event queries to track sequences of events that match a given pattern. The state-of-the-art 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 Interval-Driven Semantic Caching. Techniques for incrementally loading, purging and exploiting the cache content are described. Our experimental study using real-world stock trades evaluates the performance of our proposed caching strategies for different query types.

[12] 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 firewall-analysis 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 real-world firewall-configuration languages, decomposing them into multiple policies that capture different aspects of firewall functionality. We present evaluation on networking-forum posts and on an in-use enterprise firewall-configuration.

[13] 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 type-assignment derivations inspired by the equational theory of bicartesian-closed categories.

Some supplementary material can be found here: lpar10-appendix.pdf,

[14] Timothy Nelson, Daniel J. Dougherty, Kathi Fisler, and Shriram Krishnamurthi. On the finite model property in order-sorted logic. Technical report, Worcester Polytechnic Institute, 2010. [ bib | .pdf ]
The Schoenfinkel-Bernays-Ramsey class is a fragment of first-order 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 many-sorted framework than in the one-sorted case. This paper makes a systematic study of this phenomenon in the general setting of order-sorted logic supporting overloading and empty sorts. We establish a syntactic condition generalizing the Schoenfinkel-Bernays-Ramsey form that ensures the Finite Model Property. We give a linear-time algorithm for deciding this condition and a polynomial-time algorithm for computing the bound on model sizes. As a consequence, model-finding is a complete decision procedure for sentences in this class. Our algorithms have been incorporated into Margrave, a tool for analysis of access-control and firewall policies, and are available in a standalone application suitable for analyzing input to the Alloy model finder.

[15] 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 7-11, 2010, pages 109-110, 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.

[16] 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 14-19, 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 state-of-the-art 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 real-world stock trades evaluates the performance of our proposed iterative execution strategy for different query types.

[17] 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 1-19, 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.

[18] Venkatesh Raghavan, Yali Zhu, Elke A. Rundensteiner, and Daniel J. Dougherty. Multi-join 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 7-9, 2009. Proceedings, volume 5588 of Lecture Notes in Computer Science, pages 91-106, 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 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.

[19] Daniel J. Dougherty. An improved algorithm for generating database transactions from relational algebra specifications. In Proc. 10th International Workshop on Rule-Based 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.

[20] 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 483-498, 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 transition-system semantics. Because Alloy does not intrinsically provide a notion of state, however, this interpretation is only implicit in the relational-algebra 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 state-based 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 state-transition 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.

[21] 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 ]
[22] 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 158-169, 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 non-trivial specification. We also discuss lessons learned about the relationship between Alloy specifications and imperative implementations.

[23] Daniel J. Dougherty, Silvia Ghilezan, and Pierre Lescanne. Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage. Theor. Comput. Sci., 398(1-3):114-128, 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 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.

[24] 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 375-389, 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.

[25] 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 578-593, 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. 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.

[26] Daniel J. Dougherty. Core XACML and term rewriting. Technical Report WPI-CS-TR-07-07, Worcester Polytechnic Iinstitute, 2007. [ bib | .pdf ]
We define a notion of “core” XACML policies and show how these can be represented as ground associative-commutative term rewriting systems with strategies.

[27] 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 ]
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.

[28] Daniel J. Dougherty, Kathi Fisler, and Shriram Krishnamurthi. Specifying and reasoning about dynamic access-control policies. In 3rd International Joint Conference on Automated Reasoning (IJCAR), volume 4130 of Lecture Notes in Computer Science, pages 632-646, 2006. [ bib | .pdf ]
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.

[29] Daniel J. Dougherty, Pierre Lescanne, and Luigi Liquori. Addressed term rewriting systems: Application to a typed object calculus. Mathematical Structures in Computer Science, 16:667-709, 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 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.

[30] Murali Mani, Song Wang, Daniel J. Dougherty, and Elke A. Rundensteiner. Join minimization in XML-to-SQL 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.

[31] Daniel J. Dougherty and Claudio Gutiérrez. Normal forms and reduction for theories of binary relations. Theoretical Computer Science, 360(1-3):228-246, 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.

[32] 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.

[33] 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):57-82, 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 object-based languages, as for instance the family of languages called λ-Obja, involving both functional and object-based features.

[34] Daniel J. Dougherty, Silvia Ghilezan, and Pierre Lescanne. Intersection and union types in the λ-μ-μ  calculus. Electr. Notes Theor. Comput. Sci., 136:153-172, 2005. [ bib | .pdf ]
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.

[35] Daniel J. Dougherty and Stanley M. Selkow. The complexity of the certification of properties of stable marriage. Inf. Process. Lett., 92(6):275-277, 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.

[36] Daniel J. Dougherty, Silvia Ghilezan, and Pierre Lescanne. Characterizing strong normalization in a language with control operators. In 6th ACM-SIGPLAN 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 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.

[37] Daniel J. Dougherty and Carlos Martinez. Unification and matching modulo type isomorphism. In 2nd International Workshop on Higher-Order Rewriting, 2004. [ bib | .pdf ]
We present some initial results in an investigation of higher-order unification and matching in the presence of type isomorphism

[38] Stephane Lengrand, Pierre Lescanne, Daniel J. Dougherty, Mariangiola Dezani-Ciancaglini, and Steffen van Bakel. Intersection types for explicit substitutions. Information and Computation, 189(1):17-42, 2004. [ bib | .pdf ]
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.

[39] Daniel J. Dougherty and Pierre Lescanne. Reductions, intersection types, and explicit substitutions. Mathematical Structures in Computer Science, 13(1):55-85, 2003. [ bib | .pdf ]
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.

[40] 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 511-524. 2nd IFIP International Conference on Theoretical Computer Science, 2002. [ bib ]
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.

[41] 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 340-351, 2002. [ bib | .pdf ]
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.

[42] 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 121-135, Krakow, Poland, 2001. [ bib | .pdf ]

[43] F. Lang, P. Lescanne, L. Liquori, Daniel J. Dougherty, and K. Rose. Obj+a, a generic object-calculus 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 ]

[44] 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 95-109, 2000. [ bib ]

[45] Daniel J. Dougherty and Ramesh Subrahmanyam. Equality between functionals in the presence of coproducts. Information and Computation, 157(1,2):52-83, 2000. [ bib | .pdf ]
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.

[46] Frederic Lang, Daniel J. Dougherty, Pierre Lescanne, Luigi Liquori, and Kristoffer Rose. Addressed term rewriting systems. Technical Report RR 1999-30, Ecole Normale Superieure de Lyon, 1999. [ bib | .pdf ]
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.

[47] F. Lang, P. Lescanne, L. Liquori, Daniel J. Dougherty, and K. Rose. A Generic Object-Calculus Based on Addressed Term Rewriting Systems. Technical Report RR1999-54, Laboratoire de l'Informatique et du Parallelisme, ENS Lyon, 1999. [ bib | .pdf ]

[48] Friedrich Otto, Paliath Narendran, and Daniel J. Dougherty. Equational unification, word unification, and 2nd-order equational unification. Theoretical Computer Science, 198(1-2):1-47, 1998. [ bib | .pdf ]
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.

[49] 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 282-291, San Diego, California, 1995. IEEE Computer Society Press. [ bib ]

[50] 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 367-381, 1995. [ bib ]

[51] Daniel J. Dougherty and Patricia Johann. A combinatory logic approach to higher-order E-unification. Theoretical Computer Science, 139(1-2):207-242, 1995. [ bib | .pdf ]
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.

[52] 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 137-151, Berlin, 1993. Springer-Verlag. [ 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 (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.

[53] Daniel J. Dougherty. Closed categories and categorial grammar. Notre Dame Journal of Formal Logic, 34(1):36-49, 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 syntax-category and a semantics-category, the fundamental properties of biclosed categories induce a rudimentary computationally oriented theory of language.

[54] Daniel J. Dougherty. Higher-order unification via combinators. Theoretical Computer Science, 114(2):273-298, 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 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.

[55] Daniel J. Dougherty and Patricia Johann. A combinatory logic approach to higher-order E-Unification. In Deepak Kapur, editor, Proc. 11th International Conference on Automated Deduction (CADE-11), volume 607 of Lecture Notes in Artificial Intelligence, pages 79-93, Saratoga Springs, NY, 1992. [ bib ]

[56] Daniel J. Dougherty and Patricia Johann. An improved general E-unification method. Journal of Symbolic Computation, 14(4):303-320, 1992. [ bib | .pdf ]
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.

[57] Daniel J. Dougherty. Adding algebraic rewriting to the untyped lambda calculus. Information and Computation, 101(2):251-267, 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 beta-reduction plus rewriting; we sketch the application to the polymorphic lambda calculus.

[58] 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 37-48, 1991. [ bib ]

[59] Daniel J. Dougherty. A strong Baire category theorem for products. Topology and Its Applications, 39:105-112, 1991. [ bib ]

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

[61] Daniel J. Dougherty. Decomposition of infinite matrices. Journal of Combinatorial Theory (Series A), 45:277-289, 1987. [ bib ]

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

[63] Daniel J. Dougherty. Gentzen systems, resolution, and literal trees. Notre Dame Journal of Formal Logic, 27:483-503, 1986. [ bib ]


This file was generated by bibtex2html 1.96.