@INPROCEEDINGS{w_rule09,
author = {Daniel J.\ Dougherty},
title = {An Improved Algorithm for Generating Database
Transactions from Relational Algebra Specifications},
booktitle = {Proc. 10th International Workshop on Rule-Based
Programming (RULE)},
year = 2009,
abstract = {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.},
note = {to appear},
pdf = {rule09.pdf}
}
@INPROCEEDINGS{c_fm09,
author = {Theophilos Giannakopoulos and Daniel J.\ Dougherty and
Kathi Fisler and Shriram Krishnamurthi},
title = {Towards an Operational Semantics for {A}lloy},
booktitle = {Proc. 16th International Symposium on Formal Methods},
year = 2009,
abstract = {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.},
note = {to appear},
pdf = {fm09.pdf}
}
@PROCEEDINGS{e_secret08,
title = {Proceedings of the Third International Workshop on
Security and Rewriting Techniques (SecReT 2008)},
editor = {Daniel J. Dougherty and Santiago Escobar},
series = {Electronic Notes in Theoretical Computer Science},
volume = 234,
year = 2009,
issn = {1571-0661}
}
@INPROCEEDINGS{c_bncod09,
author = {Venkatesh Raghavan and Yali Zhu and Elke
A. Rundensteiner and Daniel J. Dougherty},
title = {Multi-Join Continuous Query Optimization: Covering the
Spectrum of Linear, Acyclic, and Cyclic Queries},
booktitle = {Proc. 26th British National Conference on Databases},
year = 2009,
abstract = {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 {\it 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 {\it 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 {\it
Q-Aware} approach that selects the optimization
algorithm used for generating the join order, based on
the shape of the query.},
pdf = {bncod09.pdf}
}
@INPROCEEDINGS{c_fse08,
author = {Shriram Krishnamurthi and Daniel J. Dougherty and
Kathi Fisler and Daniel Yoo},
title = {Alchemy: Transmuting Base {A}lloy Specifications into
Implementations},
booktitle = {ACM SIGSOFT International Symposium on the Foundations
of Software Engineering},
year = 2008,
abstract = { 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.},
pdf = {fse08.pdf}
}
@ARTICLE{a_fest07,
author = {Daniel J. Dougherty and Silvia Ghilezan and Pierre
Lescanne},
title = {Characterizing strong normalization in the
{C}urien-{H}erbelin symmetric lambda calculus:
extending the {C}oppo-{D}ezani heritage},
journal = {Theor. Comput. Sci.},
volume = 398,
number = {1-3},
year = 2008,
issn = {0304-3975},
pages = {114--128},
publisher = {Elsevier Science Publishers Ltd.},
address = {Essex, UK},
abstract = {We develop an intersection type system for the
\lambda-\mu-\mu~ 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.},
pdf = {CDR-festschrift.pdf}
}
@INPROCEEDINGS{c_dfk_esorics07,
author = {Daniel J. Dougherty and Kathi Fisler and Shriram
Krishnamurthi},
title = {Obligations and their Interaction with Programs},
booktitle = {12th European Symposium On Research In Computer
Security (ESORICS)},
series = {Lecture Notes in Computer Science},
volume = 4734,
year = 2007,
pages = {375--389},
month = {September},
abstract = {Obligations are pervasive in modern systems, often
linked to access control decisions. We present a very
general model of obligations as objects with state,
and discuss its interaction with 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.},
pdf = {dfk-esorics07.pdf}
}
@INPROCEEDINGS{c_dkks_esorics07,
author = {Daniel J. Dougherty and Claude Kirchner and Helene
Kirchner and Anderson Santana de Oliveira},
title = {Modular Access Control via Strategic Rewriting},
booktitle = {12th European Symposium On Research In Computer
Security (ESORICS)},
series = {Lecture Notes in Computer Science},
volume = 4734,
year = 2007,
pages = {578--593},
month = {September},
abstract = {Security policies, in particular access control, are
fundamental elements of computer security. We address
the problem of authoring and analyzing policies in a
modular way using techniques 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.},
pdf = {dkks-esorics07.pdf}
}
@TECHREPORT{tr_07,
author = {Daniel J. Dougherty},
title = {Core {XACML} and Term Rewriting},
institution = {Worcester Polytechnic Iinstitute},
year = 2007,
number = {WPI-CS-TR-07-07},
abstract = {We define a notion of ``core'' XACML and show how
these can be represented as ground
associative-commutative term rewriting systems with
strategies.},
pdf = {xacml-and-trs.pdf}
}
@INPROCEEDINGS{c_wst07,
author = {Daniel J. Dougherty and Silvia Ghilezan and Pierre
Lescanne},
title = {A General Technique for Analyzing Termination in
Symmetric Proof Calculi},
booktitle = {9th International Workshop on Termination (WST)},
year = 2007,
month = {July},
abstract = {Proof-term calculi expressing a computational
interpretation of classical logic serve as tools for
extracting the constructive content of classical
proofs and at the same time can be seen 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.},
pdf = {wst07.pdf}
}
@INPROCEEDINGS{c_ijcar_06,
author = {Daniel J. Dougherty and Kathi Fisler and
Shriram Krishnamurthi},
title = {Specifying and Reasoning about Dynamic
Access-Control Policies},
booktitle = {3rd International Joint Conference on Automated
Reasoning (IJCAR)},
series = {Lecture Notes in Computer Science},
volume = 4130,
year = 2006,
pages = {632--646},
abstract = {Access-control policies have grown from simple
matrices to non-trivial specifications written
in sophisticated languages. The increasing
complexity of these policies demands
correspondingly 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. },
pdf = {ijcar06.pdf}
}
@ARTICLE{a_mscs_06,
author = {Daniel J. Dougherty and Pierre Lescanne and
Luigi Liquori},
title = {Addressed Term Rewriting Systems: Application
to a Typed Object Calculus},
journal = {Mathematical Structures in Computer Science},
year = 2006,
volume = 16,
pages = {667--709},
abstract = {We present a formalism called \emph{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.},
pdf = {lambda-obj-mscs.pdf}
}
@ARTICLE{a_sigmod06,
author = {Murali Mani and Song Wang and Daniel
J. Dougherty and Elke A. Rundensteiner},
title = { Join Minimization in {XML}-to-{SQL} Translation:
An Algebraic Approach.},
journal = {Bulletin of ACM SIGMOD},
volume = {35},
number = {1},
month = {March},
year = {2006},
abstract = {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. },
pdf = {sigmod06.pdf}
}
@ARTICLE{a_relations_tcs_06,
author = {Daniel J. Dougherty and Claudio Guti\'{e}rrez},
title = {Normal Forms and Reduction for Theories of
Binary Relations},
journal = {Theoretical Computer Science},
year = 2006,
abstract = {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. },
volume = 360,
number = {1--3},
pages = {228--246},
pdf = {relations-tcs.pdf}
}
@INPROCEEDINGS{c_rta00,
author = {Daniel J.\ Dougherty and Claudio Guti\'{e}rrez},
title = {Normal Forms and Reduction for Theories of Binary
Relations},
pages = {95--109},
year = 2000,
abstract = {},
booktitle = {Proc.\ Eleventh Intl.\ Conf.\ on Rewriting Techniques
and Applications (RTA)},
volume = 1833,
series = {Lecture Notes in Computer Science}
}
@INPROCEEDINGS{c_lpar_05,
author = {Daniel J. Dougherty and Silvia Ghilezan and
Silvia Likavec and Pierre Lescanne},
title = {Strong normalization of the dual classical
sequent calculus},
booktitle = {12th International Conference on Logic for
Programming, Artificial Intelligence and
Reasoning (LPAR)},
year = 2005,
abstract = {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 \lambda-\mu 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.},
pdf = {lpar05.pdf}
}
@ARTICLE{a_entcs_05a,
author = {Daniel J. Dougherty and Pierre Lescanne and
Luigi Liquori and Frederic Lang},
title = {Addressed Term Rewriting Systems: Syntax,
Semantics, and Pragmatics: Extended Abstract.},
journal = {Electr. Notes Theor. Comput. Sci.},
volume = 127,
number = 5,
year = 2005,
pages = {57-82},
abstract = { We present a formalism called \emph{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 \lambda-Obja,
involving both functional and object-based
features.},
ee = {http://dx.doi.org/10.1016/j.entcs.2004.12.042},
pdf = {entcs05-termgraph.pdf}
}
@ARTICLE{a_entcs_05b,
author = {Daniel J. Dougherty and Silvia Ghilezan and
Pierre Lescanne},
title = {Intersection and Union Types in the
\lambda-\mu-\mu~ calculus.},
journal = {Electr. Notes Theor. Comput. Sci.},
volume = 136,
year = 2005,
pages = {153-172},
abstract = {The original \lambda-\mu-\mu\; 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.},
ee = {http://dx.doi.org/10.1016/j.entcs.2005.06.010},
pdf = {entcs05-ITRS.pdf}
}
@ARTICLE{a_ipl04,
author = {Daniel J. Dougherty and Stanley M. Selkow},
title = {The complexity of the certification of
properties of Stable Marriage.},
journal = {Inf. Process. Lett.},
volume = {92},
number = {6},
year = {2004},
pages = {275-277},
ee = {http://dx.doi.org/10.1016/j.ipl.2004.09.006},
abstract = { We give some lower bounds on the certificate
complexity of some problems concerning stable
marriage, answering a question of Gusfield and
Irving.},
pdf = {ipl.pdf}
}
@INPROCEEDINGS{c_ppdp04,
author = {Daniel J. Dougherty and Silvia Ghilezan and
Pierre Lescanne},
title = {Characterizing strong normalization in a
language with control operators},
booktitle = {6th ACM-SIGPLAN International Conference on
Principles and Practice of Declarative
Programming (PPDP)},
year = 2004,
abstract = {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.},
pdf = {ppdp04.pdf}
}
@INPROCEEDINGS{w_hor04,
author = {Daniel J. Dougherty and Carlos Martinez},
title = {Unification and matching modulo type
isomorphism},
booktitle = {2nd International Workshop on Higher-Order
Rewriting},
year = 2004,
pdf = {hor04.pdf},
abstract = {We present some initial results in an
investigation of higher-order unification and
matching in the presence of type isomorphism}
}
@ARTICLE{a_iandc04,
author = {Stephane Lengrand and Pierre Lescanne and
Daniel J.\ Dougherty and Mariangiola
Dezani-Ciancaglini and Steffen van Bakel},
title = {Intersection types for explicit substitutions },
journal = {Information and Computation},
year = 2004,
volume = 189,
number = 1,
pages = {17--42},
abstract = {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. },
pdf = {iandc04.pdf}
}
@ARTICLE{a_mscs03,
author = {Daniel J.\ Dougherty and Pierre Lescanne},
title = {Reductions, intersection types, and explicit
substitutions},
journal = {Mathematical Structures in Computer Science},
year = 2003,
volume = 13,
number = 1,
pages = {55--85},
abstract = { 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. },
pdf = {mscs03.pdf}
}
@INPROCEEDINGS{c_tcs02,
author = {Daniel J.\ Dougherty and Pierre Lescanne and
St\'ephane Lengrand},
title = {An improved system of intersection types for
explicit substitutions},
booktitle = {Proc. Conf. Foundations of Information
Technology in the Era of Network and Mobile
Computing},
pages = {511--524},
year = 2002,
organization = {2nd IFIP International Conference on
Theoretical Computer Science},
abstract = { 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. }
}
@INPROCEEDINGS{c_tlca01,
author = {Daniel J.\ Dougherty and Pierre Lescanne},
title = {Reductions, intersection types, and explicit
substitutions (extended abstract)},
pages = {121-135},
year = 2001,
booktitle = {Proc.\ 5th Int. Conf. on Typed Lambda Calculus
and Applications (TLCA)},
editor = {S. Abramsky},
volume = 2044,
series = {Lecture Notes in Computer Science},
address = {Krakow, Poland},
month = MAY,
abstract = {},
pdf = {tlca01.pdf}
}
@INPROCEEDINGS{c_rta02,
author = {Daniel J.\ Dougherty and ToMasz Wierzbicki},
title = {A Decidable Variant of Higher Order Matching},
booktitle = {Proc.\ Thirteenth Intl.\ Conf.\ on Rewriting
Techniques and Applications (RTA)},
pages = {340--351},
year = 2002,
editor = {},
volume = 2378,
series = {Lecture Notes in Computer Science},
abstract = {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. },
pdf = {rta02.pdf}
}
@INPROCEEDINGS{w_westapp01,
author = {F. Lang and P. Lescanne and L. Liquori and
Daniel J.\ Dougherty and K. Rose},
title = {Obj+a, a generic object-calculus based on
addressed term rewriting systems with modules },
booktitle = {WESTAPP 01: The Fourth International Workshop
on Explicit Substitutions: Theory and
Applications to Programs and Proofs },
abstract = {},
year = 2001
}
@ARTICLE{a_iandc00,
author = {Daniel J.\ Dougherty and Ramesh Subrahmanyam},
title = {Equality between Functionals in the Presence of
Coproducts},
journal = {Information and Computation},
year = 2000,
volume = 157,
number = {1,2},
pages = {52--83},
abstract = {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. },
pdf = {iandc00.pdf}
}
@INPROCEEDINGS{c_lics95,
title = {Equality between Functionals in the Presence of
Coproducts},
author = {Daniel J.\ Dougherty and Ramesh Subrahmanyam},
pages = {282--291},
booktitle = {Proc.\, Tenth Annual {IEEE} Symposium on Logic
in Computer Science},
year = 1995,
month = {26--29 } # JUN,
address = {San Diego, California},
organization = {IEEE Computer Society Press},
abstract = {}
}
@TECHREPORT{t_ldllr99,
author = {Frederic Lang and Daniel J. Dougherty and
Pierre Lescanne and Luigi Liquori and
Kristoffer Rose },
title = {Addressed term rewriting systems},
institution = {Ecole Normale Superieure de Lyon},
year = 1999,
number = {RR 1999-30},
abstract = {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. },
pdf = {ldlr99.pdf}
}
@TECHREPORT{t_llldr99,
author = {F. Lang and P. Lescanne and L. Liquori and
Daniel J.\ Dougherty and K. Rose},
title = {A {G}eneric {O}bject-{C}alculus {B}ased on
{A}ddressed {T}erm {R}ewriting {S}ystems},
abstract = {},
institution = {Laboratoire de l'Informatique et du
Parallelisme, ENS Lyon},
year = 1999,
number = {RR1999-54},
pdf = {llldr99.pdf}
}
@ARTICLE{a_tcs98,
author = {Friedrich Otto and Paliath Narendran and Daniel
J.\ Dougherty},
title = {Equational unification, word unification,
and $2$nd-order equational unification},
journal = {Theoretical Computer Science},
volume = 198,
number = {1--2},
pages = {1--47},
day = 30,
month = MAY,
year = 1998,
abstract = { 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. },
pdf = {tcs98.pdf}
}
@INPROCEEDINGS{c_rta95,
author = {Friedrich Otto and Paliath Narendran and Daniel
J. Dougherty},
title = {Some independence results for equational
unification},
booktitle = {Proc. Sixth Intl. Conf. on Rewriting Techniques
and Applications (RTA 1995)},
pages = {367--381},
year = 1995,
volume = 914,
series = {Lecture Notes in Computer Science},
abstract = {}
}
@ARTICLE{a_tcs95,
author = {Daniel J.\ Dougherty and Patricia Johann},
title = {A combinatory logic approach to higher-order
{$E$}-unification},
journal = {Theoretical Computer Science},
volume = {139},
number = {1--2},
pages = {207--242},
day = {06},
month = MAR,
year = {1995},
issn = {0304-3975},
pubcountry = {Netherlands},
abstract = {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. },
pdf = {tcs95.pdf}
}
@INPROCEEDINGS{c_cade92,
author = {Daniel J.\ Dougherty and Patricia Johann},
title = {A Combinatory Logic Approach to Higher-Order
{{$E$}-Unification}},
pages = {79--93},
isbn = {3-540-55602-8},
editor = {Deepak Kapur},
booktitle = {Proc.\ 11th International Conference on
Automated Deduction ({CADE}-11)},
address = {Saratoga Springs, NY},
year = 1992,
series = {Lecture Notes in Artificial Intelligence},
volume = 607,
abstract = {}
}
@INPROCEEDINGS{c_rta93,
author = {Daniel J.\ Dougherty},
title = {Some lambda calculi with categorical sums and
products},
pages = {137--151},
isbn = {3-540-56868-9},
editor = {Claude Kirchner},
booktitle = {Proc.\ 5th International Conference on
Rewriting Techniques and Applications ({RTA})},
series = {Lecture Notes in Computer Science},
volume = 690,
publisher = {Springer-Verlag},
address = {Berlin},
year = 1993,
abstract = { We consider the simply typed
$\lambda$-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. },
pdf = {rta93.pdf}
}
@ARTICLE{a_ndjfl93,
title = {Closed Categories and Categorial Grammar},
author = {Daniel J.\ Dougherty},
pages = {36--49},
journal = {Notre Dame Journal of Formal Logic},
month = {Winter},
year = 1993,
volume = 34,
number = 1,
abstract = {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. },
pdf = {ndjfl93.pdf}
}
@ARTICLE{a_tcs93,
author = {Daniel J.\ Dougherty},
title = {Higher-order unification via combinators},
journal = {Theoretical Computer Science},
volume = 114,
number = 2,
pages = {273--298},
day = 21,
month = JUN,
year = 1993,
abstract = {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. },
pdf = {tcs93.pdf}
}
@ARTICLE{a_jsc92,
author = {Daniel J.\ Dougherty and Patricia Johann},
title = {An improved general ${E}$-unification method},
journal = {Journal of Symbolic Computation},
volume = 14,
number = 4,
pages = {303--320},
month = OCT,
year = 1992,
issn = {0747-7171},
abstract = {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. },
pdf = {jsc92.pdf}
}
@INPROCEEDINGS{c_cade90,
author = {Daniel J.\ Dougherty and Patricia Johann},
title = {An Improved General {$E$}-unification Method},
pages = {261--275},
booktitle = {Proc.\ 10th International Conference on
Automated Deduction, Kaiserslautern (Germany)},
year = {1990},
editor = {M. Stickel},
series = {Lecture Notes in Computer Science},
volume = {449},
month = JUL,
abstract = {}
}
@ARTICLE{a_iandc92,
title = {Adding Algebraic Rewriting to the Untyped
Lambda Calculus},
author = {Daniel J.\ Dougherty},
pages = {251--267},
journal = {Information and Computation},
month = DEC,
year = 1992,
volume = 101,
number = 2,
abstract = {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 \emph{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.},
pdf = {iandc92.pdf}
}
@INPROCEEDINGS{c_rta91,
author = {Daniel J.\ Dougherty},
title = {Adding Algebraic Rewriting to the Untyped
Lambda Calculus (Extended Abstract)},
month = APR,
year = 1991,
editor = {Ron Book},
booktitle = {Proc.\ of the Fourth International Conference
on Rewriting Techniques and Applications (Como,
Italy)},
pages = {37--48},
series = {Lecture Notes in Computer Science},
publisher = {},
volume = 488,
abstract = {}
}
@ARTICLE{a_topapp91,
author = {Daniel J. Dougherty},
title = {A strong {B}aire category theorem for products},
journal = {Topology and Its Applications},
year = 1991,
volume = 39,
abstract = {},
pages = {105--112}
}
@ARTICLE{a_jcta87,
author = {Daniel J. Dougherty},
title = {Decomposition of infinite matrices},
journal = {Journal of Combinatorial Theory (Series A)},
year = 1987,
volume = 45,
abstract = {},
pages = {277--289}
}
@ARTICLE{a_jmaa87,
author = {Daniel J. Dougherty and R. M. Shortt and
R. N. Ball},
title = {Decomposition theorems for measures},
journal = {Journal of Mathematical Analysis and
Applications},
year = 1987,
volume = 128,
abstract = {},
pages = {561--580}
}
@ARTICLE{a_ndjfl86,
author = {Daniel J. Dougherty},
title = {Gentzen systems, resolution, and literal trees},
journal = {Notre Dame Journal of Formal Logic},
year = 1986,
volume = 27,
abstract = {},
pages = {483--503}
}
This file has been generated by bibtex2html 1.85.