@string{brics =	"{BRICS}"}
@string{daimi =	"Department of Computer Science, University of Aarhus"}
@string{iesd  =	"Department of Computer Science, Institute
		  of Electronic Systems, Aalborg University"}
@string{rs    =	"Research Series"}
@string{ns    =	"Notes Series"}
@string{ls    =	"Lecture Series"}
@string{ds    =	"Dissertation Series"}

@techreport{BRICS-RS-01-55,
  author = 	 "Damian, Daniel and Danvy, Olivier",
  title = 	 "A Simple {CPS} Transformation of Control-Flow
                  Information",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-55",
  address = 	 daimi,
  month = 	 dec,
  note = 	 "18~pp. Appears in {\em Logic Journal of the
                  IGPL}, 10(2):501--515, 2002",
  keywords = 	 "Program analysis. Control-flow analysis.
                  Constraints. Continuations.
                  Continuation-passing style (CPS). CPS
                  transformation. Administrative reductions.
                  One-pass CPS transformation",
  abstract = 	 "We build on Danvy and Nielsen's first-order
                  program transformation into
                  continuation-passing style (CPS) to design a
                  new CPS transformation of flow information that
                  is simpler and more efficient than what has
                  been presented in previous work. The key to
                  simplicity and efficiency is that our CPS
                  transformation constructs the flow information
                  in one go, instead of first computing an
                  intermediate result and then exploiting it to
                  construct the flow information.\bibpar
                  More precisely, we show how to compute
                  control-flow information for CPS-transformed
                  programs from control-flow information for
                  direct-style programs and vice-versa. As a
                  corollary, we confirm that CPS transformation
                  has no effect on the control-flow information
                  obtained by constraint-based control-flow
                  analysis. The transformation has immediate
                  applications in assessing the effect of the CPS
                  transformation over other analyses such as, for
                  instance, binding-time analysis",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-54,
  author = 	 "Damian, Daniel and Danvy, Olivier",
  title = 	 "Syntactic Accidents in Program Analysis: On
                  the Impact of the {CPS} Transformation",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-54",
  address = 	 daimi,
  month = 	 dec,
  note = 	 "41~pp. To appear in the {\em Journal of
                  Functional Programming}. This report supersedes
                  the earlier BRICS report RS-00-15",
  abstract = 	 "We show that a non-duplicating transformation
                  into continuation-passing style (CPS) has no
                  effect on control-flow analysis, a positive
                  effect on binding-time analysis for traditional
                  partial evaluation, and no effect on
                  binding-time analysis for continuation-based
                  partial evaluation: a monovariant control-flow
                  analysis yields equivalent results on a
                  direct-style program and on its CPS
                  counterpart, a monovariant binding-time
                  analysis yields less precise results on a
                  direct-style program than on its CPS
                  counterpart, and an enhanced monovariant
                  binding-time analysis yields equivalent results
                  on a direct-style program and on its CPS
                  counterpart. Our proof technique amounts to
                  constructing the CPS counterpart of flow
                  information and of binding times.\bibpar
                  Our results formalize and confirm a folklore
                  theorem about traditional binding-time
                  analysis, namely that CPS has a positive effect
                  on binding times. What may be more surprising
                  is that the benefit does not arise from a
                  standard refinement of program analysis, as,
                  for instance, duplicating continuations.\bibpar
                  The present study is symptomatic of an
                  unsettling property of program analyses: their
                  quality is unpredictably vulnerable to
                  syntactic accidents in source programs, i.e.,
                  to the way these programs are written. More
                  reliable program analyses require a better
                  understanding of the effect of syntactic
                  change",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}

@techreport{BRICS-RS-01-53,
  author = 	 "{\'E}sik, Zolt{\'a}n and Ito, Masami",
  title = 	 "Temporal Logic with Cyclic Counting and the
                  Degree of Aperiodicity of Finite Automata",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-53",
  address = 	 iesd,
  month = 	 dec,
  note = 	 "31~pp",
  abstract = 	 "We define the degree of aperiodicity of finite
                  automata and show that for every set $M$ of
                  positive integers, the class ${\bf QA}_M$ of
                  finite automata whose degree of aperiodicity
                  belongs to the division ideal generated by $M$
                  is closed with respect to direct products,
                  disjoint unions, subautomata, homomorphic
                  images and renamings. These closure conditions
                  define q-varieties of finite automata. We show
                  that q-varieties are in a one-to-one
                  correspondence with literal varieties of
                  regular languages. We also characterize ${\bf
                  QA}_M$ as the cascade product of a variety of
                  counters with the variety of aperiodic (or
                  counter-free) automata. We then use the notion
                  of degree of aperiodicity to characterize the
                  expressive power of first-order logic and
                  temporal logic with cyclic counting with
                  respect to any given set $M$ of moduli. It
                  follows that when $M$ is finite, then it is
                  decidable whether a regular language is
                  definable in first-order or temporal logic with
                  cyclic counting with respect to moduli in $M$",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}

@techreport{BRICS-RS-01-52,
  author = 	 "Groth, Jens",
  title = 	 "Extracting Witnesses from Proofs of Knowledge
                  in the Random Oracle Model",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-52",
  address = 	 daimi,
  month = 	 dec,
  note = 	 "23~pp",
  abstract = 	 "We prove that a 3-move interactive proof
                  system with the special soundness property made
                  non-interactive by applying the Fiat-Shamir
                  heuristic is almost a non-interactive proof of
                  knowledge in the random oracle model. In an
                  application of the result we demonstrate that
                  the Damg{\aa}rd-Jurik voting scheme based on
                  homomorphic threshold encryption is secure
                  against a nonadaptive adversary according to
                  Canetti's definition of multi-party computation
                  security",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}

@techreport{BRICS-RS-01-51,
  author = 	 "Kohlenbach, Ulrich",
  title = 	 "On Weak {M}arkov's Principle",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-51",
  address = 	 daimi,
  month = 	 dec,
  note = 	 "10~pp. Appears in {\em Mathematical Logic
                  Quarterly}, 48(suppl.\ 1):59--65, 2002",
  keywords = 	 "Markov's principle, intuitionism, constructive
                  analysis, restricted classical logic, modified
                  realizability",
  abstract = 	 "We show that the so-called weak Markov's
                  principle (WMP) which states that every
                  pseudo-positive real number is positive is
                  underivable in ${\cal T}^{\omega
                  }:=$E-HA$^{\omega}+$AC. Since ${\cal T}^{\omega
                  }$ allows to formalize (at least large parts
                  of) Bishop's constructive mathematics this
                  makes it unlikely that WMP can be proved within
                  the framework of Bishop-style mathematics
                  (which has been open for about 20 years). The
                  underivability even holds if the ineffective
                  schema of full comprehension (in all types) for
                  negated formulas (in particular for $\exists
                  $-free formulas) is added which allows to
                  derive the law of excluded middle for such
                  formulas.",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-50,
  author = 	 "Srba, Ji{\v{r}}{\'\i}",
  title = 	 "Note on the Tableau Technique for Commutative
                  Transition Systems",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-50",
  address = 	 daimi,
  month = 	 dec,
  note = 	 "19~pp. Appears in " # lncs2303 # ", pages
                  387--401",
  abstract = 	 "We define a class of transition systems called
                  effective commutative transition systems (ECTS)
                  and show, by generalising a tableau-based proof
                  for BPP, that bisimilarity between any two
                  states of such a transition system is
                  decidable. It gives a general technique for
                  extending decidability borders of strong
                  bisimilarity for a wide class of infinite-state
                  transition systems. This is demonstrated for
                  several process formalisms, namely BPP process
                  algebra, lossy BPP processes, BPP systems with
                  interrupt and timed-arc BPP nets",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-49,
  author = 	 "Danvy, Olivier and Nielsen, Lasse R.",
  title = 	 "A First-Order One-Pass {CPS} Transformation",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-49",
  address = 	 daimi,
  month = 	 dec,
  note = 	 "21~pp. To appear in {\em Theoretical Computer
                  Science}. Extended version of a paper appearing
                  in " # lncs2303 # ", pages 98--113",
  abstract = 	 "We present a new transformation of
                  call-by-value lambda-terms into
                  continuation-passing style (CPS). This
                  transformation operates in one pass and is both
                  compositional and first-order. Because it
                  operates in one pass, it directly yields
                  compact CPS programs that are comparable to
                  what one would write by hand. Because it is
                  compositional, it allows proofs by structural
                  induction. Because it is first-order, reasoning
                  about it does not require the use of a logical
                  relation.\bibpar
                  This new CPS transformation connects two
                  separate lines of research. It has already been
                  used to state a new and simpler correctness
                  proof of a direct-style transformation, and to
                  develop a new and simpler CPS transformation of
                  control-flow information",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-48,
  author = 	 "Nielsen, Mogens and Valencia, Frank D.",
  title = 	 "Temporal Concurrent Constraint Programming:
                  Applications and Behavior",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-48",
  address = 	 daimi,
  month = 	 dec,
  note = 	 "36~pp. Appears in " # lncs2300 # ", pages
                  298--321",
  abstract = 	 "The {\em ntcc} calculus is a model of
                  non-deterministic temporal concurrent
                  constraint programming. In this paper we study
                  behavioral notions for this calculus. In the
                  underlying computational model, concurrent
                  constraint processes are executed in discrete
                  time intervals. The behavioral notions studied
                  reflect the reactive interactions between
                  concurrent constraint processes and their
                  environment, as well as internal interactions
                  between individual processes. Relationships
                  between the suggested notions are studied, and
                  they are all proved to be decidable for a
                  substantial fragment of the calculus.
                  Furthermore, the expressive power of this
                  fragment is illustrated by examples",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-47,
  author = 	 "Nielsen, Jesper Buus",
  title = 	 "Non-Committing Encryption is Too Easy in the
                  Random Oracle Model",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-47",
  address = 	 daimi,
  month = 	 dec,
  note = 	 "20~pp",
  abstract = 	 "The non-committing encryption problem arises
                  in the setting of adaptively secure
                  cryptographic protocols, as the task of
                  implementing secure channels. We prove that in
                  the random oracle model, where the parties have
                  oracle access to a uniformly random function,
                  non-committing encryption can be implemented
                  efficiently using any trapdoor
                  permutation.\bibpar
                  We also prove that no matter how the oracle is
                  instantiated in practice the resulting scheme
                  will never be non-committing, and we give a
                  short discussion of the random oracle model in
                  light of this",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}

@techreport{BRICS-RS-01-46,
  author = 	 "Kristiansen, Lars",
  title = 	 "The Implicit Computational Complexity of
                  Imperative Programming Languages",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-46",
  address = 	 daimi,
  month = 	 nov,
  note = 	 "46~pp",
  abstract = 	 "During the last decade Cook, Bellantoni,
                  Leivant and others have developed the theory of
                  implicit computational complexity, i.e.\ the
                  theory of predicative recursion, tiered
                  definition schemes, etcetera. We extend and
                  modify this theory to work in a context of
                  imperative programming languages, and
                  characterise complexity classes like {\tt P},
                  {\sc linspace}, {\sc pspace} and the classes in
                  the Grzegorczyk hiearchy. Our theoretical
                  framework seems promising with respect to
                  applications in engineering.",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}

@techreport{BRICS-RS-01-45,
  author = 	 "Damg{\aa}rd, Ivan B. and Frandsen, Gudmund
                  Skovbjerg",
  title = 	 "An Extended Quadratic {F}robenius Primality
                  Test with Average Case Error Estimates",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-45",
  address = 	 daimi,
  month = 	 nov,
  note = 	 "43~pp",
  abstract = 	 "We present an Extended Quadratic Frobenius
                  Primality Test (EQFT), which is related to the
                  Miller-Rabin test and the Quadratic Frobenius
                  test (QFT) by Grantham. EQFT is well-suited for
                  generating large, random prime numbers since on
                  a random input number, it takes time about
                  equivalent to 2 Miller-Rabin tests, but has
                  much smaller error probability. EQFT extends
                  QFT by verifying additional algebraic
                  properties related to the existence of elements
                  of order 3 and 4. We obtain a simple closed
                  expression that upper bounds the probability of
                  acceptance for any input number. This in turn
                  allows us to give strong bounds on the
                  average-case behaviour of the test: consider
                  the algorithm that repeatedly chooses random
                  odd $k$ bit numbers, subjects them to $t$
                  iterations of our test and outputs the first
                  one found that passes all tests. We obtain
                  numeric upper bounds for the error probability
                  of this algorithm as well as a general closed
                  expression bounding the error. For instance, it
                  is at most $2^{-143}$ for $k=500, t=2$.
                  Compared to earlier similar results for the
                  Miller-Rabin test, the results indicates that
                  our test in the average case has the effect of
                  9 Miller-Rabin tests, while only taking time
                  equivalent to about 2 such tests. We also give
                  bounds for the error in case a prime is sought
                  by incremental search from a random starting
                  point. While EQFT is slower than the average
                  case on a small set of inputs, we present a
                  variant that is always fast, i.e. takes time
                  about 2 Miller-Rabin tests. The variant has
                  slightly larger worst case error probability
                  than EQFT, but still improves on previous
                  proposed tests",
  linkhtmlabs =  "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-44,
  author = 	 "M{\"o}ller, M. Oliver and Rue{\ss}, Harald and
                  Sorea, Maria",
  title = 	 "Predicate Abstraction for Dense Real-Time
                  Systems",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-44",
  address = 	 daimi,
  month = 	 nov,
  note = 	 "27~pp. Appears in " # entcs656,
  abstract = 	 "We propose predicate abstraction as a means
                  for verifying a rich class of safety and
                  liveness properties for dense real-time
                  systems. First, we define a restricted
                  semantics of timed systems which is
                  observationally equivalent to the standard
                  semantics in that it validates the same set of
                  $\mu$-calculus formulas without a next-step
                  operator. Then, we recast the model checking
                  problem ${\cal S} \models\varphi$ for a timed
                  automaton ${\cal S}$ and a $\mu$-calculus
                  formula $\varphi$ in terms of predicate
                  abstraction. Whenever a set of abstraction
                  predicates forms a so-called {\em basis}, the
                  resulting abstraction is strongly preserving in
                  the sense that ${\cal S}$ validates $\varphi$
                  iff the corresponding finite abstraction
                  validates this formula $\varphi$. Now, the
                  abstracted system can be checked using familiar
                  $\mu$-calculus model checking.\bibpar
                  Like the region graph construction for timed
                  automata, the predicate abstraction algorithm
                  for timed automata usually is prohibitively
                  expensive. In many cases it suffices to compute
                  an approximation of a finite bisimulation by
                  using only a subset of the basis of abstraction
                  predicates. Starting with some coarse
                  abstraction, we define a finite sequence of
                  refined abstractions that converges to a
                  strongly preserving abstraction. In each step,
                  new abstraction predicates are selected
                  nondeterministically from a finite basis.
                  Counterexamples from failed $\mu$-calculus
                  model checking attempts can be used to
                  heuristically choose a small set of new
                  abstraction predicates for refining the
                  abstraction",
  linkhtmlabs =  "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-43,
  author = 	 "Damg{\aa}rd, Ivan B. and Nielsen, Jesper
                  Buus",
  title = 	 "From Known-Plaintext Security to
                  Chosen-Plaintext Security",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-43",
  address = 	 daimi,
  month = 	 nov,
  note = 	 "18~pp",
  abstract = 	 "We present a new encryption mode for block
                  ciphers. The mode is efficient and is secure
                  against chosen-plaintext attack (CPA) already
                  if the underlying symmetric cipher is secure
                  against known-plaintext attack (KPA). We prove
                  that known (and widely used) encryption modes
                  as CBC mode and counter mode do not have this
                  property. In particular, we prove that CBC mode
                  using a KPA secure cipher is KPA secure, but
                  need not be CPA secure, and we prove that
                  counter mode using a KPA secure cipher need not
                  be even KPA secure. The analysis is done in a
                  concrete security framework",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}

@techreport{BRICS-RS-01-42,
  author = 	 "{\'E}sik, Zolt{\'a}n and Kuich, Werner",
  title = 	 "Rationally Additive Semirings",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-42",
  address = 	 iesd,
  month = 	 nov,
  note = 	 "11~pp. Appears in {\em Journal of Universal
                  Computer Science}, 8(2):173--183, 2002",
  keywords = 	 "Semiring, complete semiring, iteration
                  semiring, fixed point, power series",
  abstract = 	 "We define rationally additive semirings that
                  are a generalization of ($\omega$)\-complete
                  and ($\omega$-)continuous semirings. We prove
                  that every rationally additive semiring is an
                  iteration semiring. Moreover, we characterize
                  the semirings of rational power series with
                  coefficients in $N_\infty$, the semiring of
                  natural numbers equipped with a top element, as
                  the free rationally additive semirings",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-41,
  author = 	 "Damg{\aa}rd, Ivan B. and Nielsen, Jesper
                  Buus",
  title = 	 "Perfect Hiding and Perfect Binding Universally
                  Composable Commitment Schemes with Constant
                  Expansion Factor",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-41",
  address = 	 daimi,
  month = 	 oct,
  note = 	 "43~pp. Appears in " # lncs2442 # ", pages
                  581--596",
  abstract = 	 "Canetti and Fischlin have recently proposed
                  the security notion {\em universal
                  composability} for commitment schemes and
                  provided two examples. This new notion is very
                  strong. It guarantees that security is
                  maintained even when an unbounded number of
                  copies of the scheme are running concurrently,
                  also it guarantees non-malleability, resilience
                  to selective decommitment, and security against
                  adaptive adversaries. Both of their schemes
                  uses $\Theta(k)$ bits to commit to one bit and
                  can be based on the existence of trapdoor
                  commitments and non-malleable
                  encryption.\bibpar
                  We present new universally composable
                  commitment schemes based on the Paillier
                  cryptosystem and the Okamoto-Uchiyama
                  cryptosystem. The schemes are efficient: to
                  commit to $k$ bits, they use a constant number
                  of modular exponentiations and communicates
                  $O(k)$ bits. Further more the scheme can be
                  instantiated in either perfectly hiding or
                  perfectly binding versions. These are the first
                  schemes to show that constant expansion factor,
                  perfect hiding, and perfect binding can be
                  obtained for universally composable
                  commitments.\bibpar
                  We also show how the schemes can be applied to
                  do efficient zero-knowledge proofs of knowledge
                  that are universally composable",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-40,
  author = 	 "Damian, Daniel and Danvy, Olivier",
  title = 	 "{CPS} Transformation of Flow Information, Part
                  {II}: Administrative Reductions",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-40",
  address = 	 daimi,
  month = 	 oct,
  note = 	 "9~pp. To appear in the {\em Journal of Functional
                  Programming}. Superseeded by the BRICS
                  report RS-02-36",
  abstract = 	 "We characterize the impact of a linear
                  beta-reduction on the result of a control-flow
                  analysis. (By ``a linear beta-reduction'' we
                  mean the beta-reduction of a linear
                  lambda-abstraction, i.e., of a
                  lambda-abstraction whose parameter occurs
                  exactly once in its body.)\bibpar
                  As a corollary, we consider the administrative
                  reductions of a Plotkin-style transformation
                  into continuation-passing style (CPS), and how
                  they affect the result of a constraint-based
                  control-flow analysis and in particular the
                  least element in the space of solutions. We
                  show that administrative reductions preserve
                  the least solution. Since we know how to
                  construct least solutions, preservation of
                  least solutions solves a problem that was left
                  open in Palsberg and Wand's paper ``CPS
                  Transformation of Flow Information.''\bibpar
                  Therefore, together, Palsberg and Wand's
                  article ``CPS Transformation of Flow
                  Information'' and the present article show how
                  to map, in linear time, the least solution of
                  the flow constraints of a program into the
                  least solution of the flow constraints of the
                  CPS counterpart of this program, after
                  administrative reductions. Furthermore, we show
                  how to CPS transform control-flow information
                  in one pass",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-39,
  author = 	 "Danvy, Olivier and Goldberg, Mayer",
  title = 	 "There and Back Again",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-39",
  address = 	 daimi,
  month = 	 oct,
  note = 	 "14~pp. To appear in the proceedings of the
                  2002 ACM SIGPLAN International Conference on
                  Functional Programming",
  abstract = 	 "We illustrate a variety of programming
                  problems that seemingly require two separate
                  list traversals, but that can be efficiently
                  solved in one recursive descent, without any
                  other auxiliary storage but what can be
                  expected from a control stack. The idea is to
                  perform the second traversal when returning
                  from the first.\bibpar
                  This programming technique yields new solutions
                  to traditional problems. For example, given a
                  list of length $2n$ or $2n+1$, where $n$ is
                  unknown, we can detect whether this list is a
                  palindrome in $n+1$ recursive calls and no heap
                  allocation",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-38,
  author = 	 "{\'E}sik, Zolt{\'a}n",
  title = 	 "Free {D}e {M}organ Bisemigroups and
                  Bisemilattices",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-38",
  address = 	 iesd,
  month = 	 oct,
  note = 	 "13~pp. To appear in the journal {\em Algebra
                  Colloquium}",
  keywords = 	 "bisemigroup, bisemilattice, free algebra, De
                  Morgan's laws, cograph, series-parallel graph",
  abstract = 	 "We give a geometric representation of free De
                  Morgan bisemigroups, free commutative De Morgan
                  bisemigroups and free De Morgan bisemilattices,
                  using labeled graphs",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-37,
  author = 	 "Cramer, Ronald and Shoup, Victor",
  title = 	 "Universal Hash Proofs and a Paradigm for
                  Adaptive Chosen Ciphertext Secure Public-Key
                  Encryption",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-37",
  address = 	 daimi,
  month = 	 oct,
  note = 	 "34~pp",
  abstract = 	 "We present several new and fairly practical
                  public-key encryption schemes and prove them
                  secure against adaptive chosen ciphertext
                  attack. One scheme is based on Paillier's
                  Decision Composite Residuosity (DCR)
                  assumption, while another is based in the
                  classical Quadratic Residuosity (QR)
                  assumption. The analysis is in the standard
                  cryptographic model, i.e., the security of our
                  schemes does not rely on the Random Oracle
                  model.\bibpar
                  
                  We also introduce the notion of a universal
                  hash proof system. Essentially, this is a
                  special kind of non-interactive zero-knowledge
                  proof system for an NP language. We do not show
                  that universal hash proof systems exist for all
                  NP languages, but we do show how to construct
                  very efficient universal hash proof systems for
                  a general class of group-theoretic language
                  membership problems.\bibpar
                  
                  Given an efficient universal hash proof system
                  for a language with certain natural
                  cryptographic indistinguishability properties,
                  we show how to construct an efficient
                  public-key encryption schemes secure against
                  adaptive chosen ciphertext attack in the
                  standard model. Our construction only uses the
                  universal hash proof system as a primitive: no
                  other primitives are required, although even
                  more efficient encryption schemes can be
                  obtained by using hash functions with
                  appropriate collision-resistance properties. We
                  show how to construct efficient universal hash
                  proof systems for languages related to the DCR
                  and QR assumptions. From these we get
                  corresponding public-key encryption schemes
                  that are secure under these assumptions. We
                  also show that the Cramer-Shoup encryption
                  scheme (which up until now was the only
                  practical encryption scheme that could be
                  proved secure against adaptive chosen
                  ciphertext attack under a reasonable
                  assumption, namely, the Decision Diffie-Hellman
                  assumption) is also a special case of our
                  general theory",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}

@techreport{BRICS-RS-01-36,
  author = 	 "Brodal, Gerth St{\o}lting and Fagerberg, Rolf
                  and Jacob, Riko",
  title = 	 "Cache Oblivious Search Trees via Binary Trees
                  of Small Height",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-36",
  address = 	 daimi,
  month = 	 oct,
  note = 	 "20~pp. Appears in " # acmsoda02 # ", pages
                  39--48",
  abstract = 	 "We propose a version of cache oblivious search
                  trees which is simpler than the previous
                  proposal of Bender, Demaine and Farach-Colton
                  and has the same complexity bounds. In
                  particular, our data structure avoids the use
                  of weight balanced $B$-trees, and can be
                  implemented as just a single array of data
                  elements, without the use of pointers. The
                  structure also improves space
                  utilization.\bibpar
                  For storing $n$ elements, our proposal uses
                  $(1+\varepsilon)n$ times the element size of
                  memory, and performs searches in worst case
                  $O(\log_B n)$ memory transfers, updates in
                  amortized $O((\log^2 n)/(\varepsilon B))$
                  memory transfers, and range queries in worst
                  case $O(\log_B n + k/B)$ memory transfers,
                  where $k$ is the size of the output.\bibpar
                  The basic idea of our data structure is to
                  maintain a dynamic binary tree of height $\log
                  n+O(1)$ using existing methods, embed this tree
                  in a static binary tree, which in turn is
                  embedded in an array in a cache oblivious
                  fashion, using the van Emde Boas layout of
                  Prokop.\bibpar
                  We also investigate the practicality of cache
                  obliviousness in the area of search trees, by
                  providing an empirical comparison of different
                  methods for laying out a search tree in
                  memory.\bibpar
                  The source code of the programs, our scripts
                  and tools, and the data we present here are
                  available online under \htmladdnormallink
                  {ftp.brics.dk/RS/01/36/Experiments/}{ftp://ftp.brics.dk/RS/01/36/Experiments/}",
  linkhtmlabs =  "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-35,
  author =	 "Goldberg, Mayer",
  title =	 "A General Schema for Constructing One-Point Bases in
                  the Lambda Calculus",
  institution =	 brics,
  year =	 2001,
  type =	 rs,
  number =	 "RS-01-35",
  address =	 daimi,
  month =	 sep,
  note =	 "8~pp",
  keywords =	 "Lambda calculi; Bases; Constants; Scheme Programming
                  Language",
  abstract =	 "In this paper, we present a schema for constructing
                  one-point bases for recursively enumerable sets of
                  lambda terms. The novelty of the approach is that we
                  make no assumptions about the terms for which the
                  one-point basis is constructed: They need not be
                  combinators and they may contain constants and free
                  variables. The significance of the construction is
                  twofold: In the context of the lambda calculus, it
                  characterises one-point bases as ways of
                  ``packaging'' sets of terms into a single term; And
                  in the context of realistic programming languages,
                  it implies that we can define a single procedure
                  that generates any given recursively enumerable set
                  of procedures, constants and free variables in a
                  given programming language",
  linkhtmlabs =	 "",
  linkdvi =	 "",
  linkps =	 "",
  linkpdf =	 ""
}

@techreport{BRICS-RS-01-34,
  author = 	 "Rodler, Flemming Friche and Pagh, Rasmus",
  title = 	 "Fast Random Access to Wavelet Compressed
                  Volumetric Data Using Hashing",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-34",
  address = 	 daimi,
  month = 	 aug,
  note = 	 "31~pp. To appear in {\em{ACM} Transactions on
                  Graphics}",
  abstract = 	 "We present a new approach to lossy storage of
                  the coefficients of wavelet transformed data.
                  While it is common to store the coefficients of
                  largest magnitude (and let all other
                  coefficients be zero), we allow a slightly
                  different set of coefficients to be stored.
                  This brings into play a recently proposed
                  hashing technique that allows space efficient
                  storage and very efficient retrieval of
                  coefficients. Our approach is applied to
                  compression of volumetric data sets. For the
                  ``Visible Man'' volume we obtain up to 80\%
                  improvement in compression ratio over
                  previously suggested schemes. Further, the time
                  for accessing a random voxel is quite
                  competitive",
  linkhtmlabs =  "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-33,
  author = 	 "Pagh, Rasmus and Rodler, Flemming Friche",
  title = 	 "Lossy Dictionaries",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-33",
  address = 	 daimi,
  month = 	 aug,
  note = 	 "14~pp. Short version appears in " # lncs2161 #
                  ", pages 300--311",
  abstract = 	 "Bloom filtering is an important technique for
                  space efficient storage of a conservative
                  approximation of a set $S$. The set stored may
                  have up to some specified number of ``false
                  positive'' members, but all elements of $S$ are
                  included. In this paper we consider {\em lossy
                  dictionaries\/} that are also allowed to have
                  ``false negatives'', i.e., leave out elements
                  of $S$. The aim is to maximize the weight of
                  included keys within a given space constraint.
                  This relaxation allows a very fast and simple
                  data structure making almost optimal use of
                  memory. Being more time efficient than Bloom
                  filters, we believe our data structure to be
                  well suited for replacing Bloom filters in some
                  applications. Also, the fact that our data
                  structure supports information associated to
                  keys paves the way for new uses, as illustrated
                  by an application in lossy image compression",
  linkhtmlabs =  "",
  linkps = 	 "",
  linkpdf = 	 ""
}

@techreport{BRICS-RS-01-32,
  author = 	 "Pagh, Rasmus and Rodler, Flemming Friche",
  title = 	 "Cuckoo Hashing",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-32",
  address = 	 daimi,
  month = 	 aug,
  note = 	 "21~pp. Short version appears in " # lncs2161 #
                  ", pages 121--133",
  abstract = 	 "We present a simple and efficient dictionary
                  with worst case constant lookup time, equaling
                  the theoretical performance of the classic
                  dynamic perfect hashing scheme of
                  Dietzfelbinger et al. ({\em Dynamic perfect
                  hashing: Upper and lower bounds. SIAM
                  J.\ Comput., 23(4):738--761, 1994}). The space
                  usage is similar to that of binary search
                  trees, i.e., three words per key on average.
                  The practicality of the scheme is backed by
                  extensive experiments and comparisons with
                  known methods, showing it to be quite
                  competitive also in the average case",
  linkhtmlabs =  "",
  linkps = 	 "",
  linkpdf = 	 ""
}

@techreport{BRICS-RS-01-31,
  author = 	 "Danvy, Olivier and Nielsen, Lasse R.",
  title = 	 "Syntactic Theories in Practice",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-31",
  address = 	 daimi,
  month = 	 jul,
  note = 	 "37~pp. Extended version of an article to
                  appear in the informal proceedings of the {\em
                  Second International Workshop on Rule-Based
                  Programming}, RULE 2001 (Firenze, Italy,
                  September 4, 2001). Superseeded by the BRICS
                  report RS-02-4",
  abstract = 	 "The evaluation function of a syntactic theory
                  is canonically defined as the transitive
                  closure of (1) decomposing a program into an
                  evaluation context and a redex, (2) contracting
                  this redex, and (3) plugging the result in the
                  context. Directly implementing this evaluation
                  function therefore yields an interpreter with a
                  quadratic time factor over its input. We
                  present sufficient conditions over a syntactic
                  theory to circumvent this quadratic factor, and
                  illustrate the method with two
                  programming-language interpreters and a
                  transformation into continuation-passing style
                  (CPS). In particular, we mechanically change
                  the time complexity of this CPS transformation
                  from quadratic to linear",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-30,
  author = 	 "Nielsen, Lasse R.",
  title = 	 "A Selective {CPS} Transformation",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-30",
  address = 	 daimi,
  month = 	 jul,
  note = 	 "24~pp. Appears in " # entcsmfps01 # ". A
                  preliminary version appeared in " # ns012 # ",
                  pages 201--222",
  abstract = 	 "The CPS transformation makes all functions
                  continuation-passing, uniformly. Not all
                  functions, however, need continuations: they
                  only do if their evaluation includes
                  computational effects. In this paper we focus
                  on control operations, in particular ``call
                  with current continuation'' and ``throw''. We
                  characterize this involvement as a control
                  effect and we present a selective CPS
                  transformation that makes functions and
                  expressions continuation-passing if they have a
                  control effect, and that leaves the rest of the
                  program in direct style. We formalize this
                  selective CPS transformation with an
                  operational semantics and a simulation theorem
                  {\`a} la Plotkin",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-29,
  author = 	 "Danvy, Olivier and Grobauer, Bernd and Rhiger,
                  Morten",
  title = 	 "A Unifying Approach to Goal-Directed
                  Evaluation",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-29",
  address = 	 daimi,
  month = 	 jul,
  note = 	 "23~pp. Appears in {\em New Generation
                  Computing}, 20(1):53--73, November 2001. A
                  preliminary version appeared in " # lncs2196 #
                  ", pages 108--125",
  abstract = 	 "Goal-directed evaluation, as embodied in Icon
                  and Snobol, is built on the notions of
                  backtracking and of generating successive
                  results, and therefore it has always been
                  something of a challenge to specify and
                  implement. In this article, we address this
                  challenge using computational monads and
                  partial evaluation.\bibpar
                  We consider a subset of Icon and we specify it
                  with a monadic semantics and a list monad. We
                  then consider a spectrum of monads that also
                  fit the bill, and we relate them to each other.
                  For example, we derive a continuation monad as
                  a Church encoding of the list monad. The
                  resulting semantics coincides with Gudeman's
                  continuation semantics of Icon.\bibpar
                  We then compile Icon programs by specializing
                  their interpreter (i.e., by using the first
                  Futamura projection), using type-directed
                  partial evaluation. Through various back ends,
                  including a run-time code generator, we
                  generate ML code, C code, and OCaml byte code.
                  Binding-time analysis and partial evaluation of
                  the continuation-based interpreter
                  automatically give rise to C programs that
                  coincide with the result of Proebsting's
                  optimized compiler",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-28,
  author = 	 "Aceto, Luca and {\'E}sik, Zolt{\'a}n and
                  Ing{\'o}lfsd{\'o}ttir, Anna",
  title = 	 "A Fully Equational Proof of {P}arikh's
                  Theorem",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-28",
  address = 	 daimi,
  month = 	 jun,
  note = 	 "28~pp. Appears in {\sl RAIRO, Theoretical
                  Informatics and Applications}, 36(2):129--153,
                  2002, special issue devoted to selected papers
                  from FICS 2001 (A.~Labella ed.).",
  abstract = 	 "We show that the validity of Parikh's theorem
                  for context-free languages depends only on a
                  few equational properties of least pre-fixed
                  points. Moreover, we exhibit an infinite basis
                  of $\mu$-term equations of continuous
                  commutative idempotent semirings",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-27,
  author = 	 "C{\'a}ccamo, Mario Jos{\'e} and Winskel,
                  Glynn",
  title = 	 "A Higher-Order Calculus for Categories",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-27",
  address = 	 daimi,
  month = 	 jun,
  note = 	 "24~pp. Appears in " # lncs2152 # ", pages
                  136--153",
  abstract = 	 "A calculus for a fragment of category theory
                  is presented. The types in the language denote
                  categories and the expressions functors. The
                  judgements of the calculus systematise
                  categorical arguments such as: an expression is
                  functorial in its free variables; two
                  expressions are naturally isomorphic in their
                  free variables. There are special binders for
                  limits and more general ends. The rules for
                  limits and ends support an algebraic
                  manipulation of universal constructions as
                  opposed to a more traditional diagrammatic
                  approach. Duality within the calculus and
                  applications in proving continuity are
                  discussed with examples. The calculus gives a
                  basis for mechanising a theory of categories in
                  a generic theorem prover like Isabelle",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-26,
  author = 	 "Frendrup, Ulrik and Jensen, Jesper Nyholm",
  title = 	 "A Complete Axiomatization of Simulation for
                  Regular {CCS} Expressions",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-26",
  address = 	 iesd,
  month = 	 jun,
  note = 	 "18~pp",
  abstract = 	 "This paper gives axiomatizations of strong and
                  weak simulation over regular CCS expressions.
                  The proof of completeness of the axiomatization
                  of strong simulation is inspired by Milner's
                  proof of completeness of his axiomatization for
                  strong equivalence over regular CCS
                  expressions. Soundness and completeness of the
                  axiomatization for weak simulation is easily
                  deduced from the corresponding result for the
                  axiomatization of strong simulation over
                  regular CCS expressions",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-25,
  author = 	 "Grobauer, Bernd",
  title = 	 "Cost Recurrences for {DML} Programs",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-25",
  address = 	 daimi,
  month = 	 jun,
  note = 	 "51~pp. Extended version of a paper appearing
                  in " # acmicfp01 # ", pages 253--264",
  abstract = 	 "A cost recurrence describes an upper bound for
                  the running time of a program in terms of the
                  size of its input. Finding cost recurrences is
                  a frequent intermediate step in complexity
                  analysis, and this step requires an abstraction
                  from data to data size. In this article, we use
                  information contained in dependent types to
                  achieve such an abstraction: Dependent ML
                  (DML), a conservative extension of ML, provides
                  dependent types that can be used to associate
                  data with size information, thus describing a
                  possible abstraction. We systematically extract
                  cost recurrences from first-order DML programs,
                  guiding the abstraction from data to data size
                  with information contained in DML type
                  derivations",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-24,
  author =	 "{\'E}sik, Zolt{\'a}n and N{\'e}meth, Zolt{\'a}n L.",
  title =	 "Automata on Series-Parallel Biposets",
  institution =	 brics,
  year =	 2001,
  type =	 rs,
  number =	 "RS-01-24",
  address =	 iesd,
  month =	 jun,
  note =	 "15~pp. Appears in " # lncs2295 # ", pages
                  217--227. Superseded by the later report
                  \htmladdnormallink{BRICS
                  RS-02-44}{http://www.brics.dk/RS/02/44/}",
  abstract =	 "We provide the basics of a 2-dimensional theory of
                  automata on series-parallel biposets. We define
                  recognizable, regular and rational sets of
                  series-parallel biposets and study their
                  relationship. Moreover, we relate these classes to
                  languages of series-parallel biposets definable in
                  monadic second-order logic"
}
@techreport{BRICS-RS-01-23,
  author = 	 "Danvy, Olivier and Nielsen, Lasse R.",
  title = 	 "Defunctionalization at Work",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-23",
  address = 	 daimi,
  month = 	 jun,
  note = 	 "45~pp. Extended version of an article
                  appearing in " # acmppdp01 # ", pages
                  162--174",
  abstract = 	 "We study practical applications of Reynolds's
                  defunctionalization technique, which is a
                  whole-program transformation from higher-order
                  to first-order functional programs. This study
                  leads us to discover new connections between
                  seemingly unrelated higher-order and
                  first-order specifications and their
                  correctness proofs. We thus perceive
                  defunctionalization both as a springboard and
                  as a bridge: as a springboard for discovering
                  new connections between the first-order world
                  and the higher-order world; and as a bridge for
                  transferring existing results between
                  first-order and higher-order settings",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-22,
  author = 	 "{\'E}sik, Zolt{\'a}n",
  title = 	 "The Equational Theory of Fixed Points with
                  Applications to Generalized Language Theory",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-22",
  address = 	 iesd,
  month = 	 jun,
  note = 	 "21~pp. Appears in " # lncs2295 # ",pages
                  21--36",
  abstract = 	 "We review the rudiments of the equational
                  logic of (least) fixed points and provide some
                  of its applications for axiomatization problems
                  with respect to regular languages, tree
                  languages, and synchronization trees",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-21,
  author = 	 "Aceto, Luca and {\'E}sik, Zolt{\'a}n and
                  Ing{\'o}lfsd{\'o}ttir, Anna",
  title = 	 "Equational Theories of Tropical Semirings",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-21",
  address = 	 iesd,
  month = 	 jun,
  note = 	 "52~pp. To appear in {\sl Theoretical Computer
                  Science}. Extended abstracts of parts of this
                  paper have appeared in " # lncs2030 # ", pages
                  42--56 and in " # ifacmaxplus01,
  abstract = 	 "This paper studies the equational theory of
                  various exotic semirings presented in the
                  literature. Exotic semirings are semirings
                  whose underlying carrier set is some subset of
                  the set of real numbers equipped with binary
                  operations of minimum or maximum as sum, and
                  addition as product. Two prime examples of such
                  structures are the {\sl$(\max,+)$ semiring} and
                  the {\sl tropical semiring}. It is shown that
                  none of the exotic semirings commonly
                  considered in the literature has a finite basis
                  for its equations, and that similar results
                  hold for the commutative idempotent weak
                  semirings that underlie them. For each of these
                  commutative idempotent weak semirings, the
                  paper offers characterizations of the equations
                  that hold in them, decidability results for
                  their equational theories, explicit
                  descriptions of the free algebras in the
                  varieties they generate, and relative
                  axiomatization results",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-20,
  author = 	 "Palamidessi, Catuscia and Valencia, Frank D.",
  title = 	 "A Temporal Concurrent Constraint Programming
                  Calculus",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-20",
  address = 	 daimi,
  month = 	 jun,
  note = 	 "31~pp. Appears in " # lncs2239 # ", pages
                  302--316",
  abstract = 	 "The tcc model is a formalism for reactive
                  concurrent constraint programming. In this
                  paper we propose a model of temporal concurrent
                  constraint programming which adds to tcc the
                  capability of modeling asynchronous and
                  non-deterministic timed behavior. We call this
                  tcc extension the ntcc calculus. The
                  expressiveness of ntcc is illustrated by
                  modeling cells and asynchronous bounded
                  broadcasting, by specifying temporal
                  requirements such as response and invariance,
                  and by modeling timed systems such as RCX
                  controllers. We present a denotational
                  semantics for modeling the
                  strongest-postcondition behavior of ntcc
                  processes, and, based on this semantics, we
                  develop a proof system for proving linear
                  temporal properties of these processes",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-19,
  author = 	 "Srba, Ji{\v{r}}{\'\i}",
  title = 	 "On the Power of Labels in Transition Systems",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-19",
  address = 	 daimi,
  month = 	 jun,
  note = 	 "23~pp. Full and extended version of " #
                  lncs2154 # ", pages 277--291",
  abstract = 	 "In this paper we discuss the role of labels in
                  transition systems with regard to bisimilarity
                  and model checking problems. We suggest a
                  general reduction from labelled transition
                  systems to unlabelled ones, preserving
                  bisimilarity and satisfiability of mu-calculus
                  formulas. We apply the reduction to the class
                  of transition systems generated by Petri nets
                  and pushdown automata, and obtain several
                  decidability/complexity corollaries for
                  unlabelled systems. Probably the most
                  interesting result is undecidability of strong
                  bisimilarity for unlabelled Petri nets.",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-18,
  author = 	 "Hangos, Katalin M. and Tuza, Zsolt and Yeo,
                  Anders",
  title = 	 "Some Complexity Problems on Single Input
                  Double Output Controllers",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-18",
  address = 	 daimi,
  month = 	 may,
  note = 	 "27~pp",
  abstract = 	 "We investigate the time complexity of
                  constructing single input double output state
                  feedback controller structures, given the
                  directed structure graph $G$ of a system. Such
                  a controller structure defines a restricted
                  type of $P_3$-partition of the graph $G$. A
                  necessary condition $(*)$ has been found and
                  two classes of graphs have been identified
                  where the search problem of finding a feasible
                  $P_3$-partition is polynomially solvable and,
                  in addition, $(*)$ is not only necessary but
                  also sufficient for the existence of a
                  $P_3$-partition. It is shown further that the
                  decision problem on two particular graph
                  classes --- defined in terms of forbidden
                  subgraphs --- remains {\it NP\/}-com\-plete,
                  but is polynomially solvable on the
                  intersection of those two classes. Moreover,
                  for every natural number $m$, a stabilizing
                  structure with Single Input $m$-Output
                  controllers can be found in polynomial time for
                  the system in question, if it admits one",
  linkhtmlabs =  "",
  linkps = 	 "",
  linkpdf = 	 ""
}

@techreport{BRICS-RS-01-17,
  author = 	 "Brabrand, Claus and M{\o}ller, Anders and
                  Olesen, Steffan and Schwartzbach, Michael I.",
  title = 	 "Language-Based Caching of Dynamically
                  Generated {HTML}",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-17",
  address = 	 daimi,
  month = 	 may,
  note = 	 "18~pp. Appears in {\em World Wide Web
                  Journal}, 5(4):305--323, 2002",
  abstract = 	 "Increasingly, HTML documents are dynamically
                  generated by interactive Web services. To
                  ensure that the client is presented with the
                  newest versions of such documents it is
                  customary to disable client caching causing a
                  seemingly inevitable performance penalty. In
                  the {\tt} system, dynamic HTML
                  documents are composed of higher-order
                  templates that are plugged together to
                  construct complete documents. We show how to
                  exploit this feature to provide an automatic
                  fine-grained caching of document templates,
                  based on the service source code. A {\tt
                  } service transmits not the full HTML
                  document but instead a compact JavaScript
                  recipe for a client-side construction of the
                  document based on a static collection of
                  fragments that can be cached by the browser in
                  the usual manner. We compare our approach with
                  related techniques and demonstrate on a number
                  of realistic benchmarks that the size of the
                  transmitted data and the latency may be reduced
                  significantly.",
  linkhtmlabs =  "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-16,
  author = 	 "Danvy, Olivier and Rhiger, Morten and Rose,
                  Kristoffer H.",
  title = 	 "Normalization by Evaluation with Typed
                  Abstract Syntax",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-16",
  address = 	 daimi,
  month = 	 may,
  note = 	 "9~pp. Appears in {\em Journal of Functional
                  Programming}, 11(6):673--68, November 2000",
  abstract = 	 "We present a simple way to implement typed
                  abstract syntax for the lambda calculus in
                  Haskell, using phantom types, and we specify
                  normalization by evaluation (i.e.,
                  type-directed partial evaluation) to yield this
                  typed abstract syntax. Proving that
                  normalization by evaluation preserves types and
                  yields normal forms then reduces to
                  type-checking the specification",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-15,
  author = 	 "Santocanale, Luigi",
  title = 	 "A Calculus of Circular Proofs and its
                  Categorical Semantics",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-15",
  address = 	 daimi,
  month = 	 may,
  note = 	 "30~pp. Appears in " # lncs2303 # ", pages
                  129--143",
  abstract = 	 "We present a calculus of proofs, the intended
                  models of which are categories with finite
                  products and coproducts, initial algebras and
                  final coalgebras of functors that are
                  recursively constructible out of these
                  operations, that is, $\mu$-bicomplete
                  categories. The calculus satisfies the cut
                  elimination and its main characteristic is that
                  the underlying graph of a proof is allowed to
                  contain a certain amount of cycles. To each
                  proof of the calculus we associate a system of
                  equations which has a meaning in every $\mu
                  $-bicomplete category. We prove that this
                  system admits always a unique solution, and by
                  means of this theorem we define the semantics
                  of the calculus",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-14,
  author = 	 "Kohlenbach, Ulrich and Oliva, Paulo B.",
  title = 	 "Effective Bounds on Strong Unicity in
                  {$L_1$}-Approximation",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-14",
  address = 	 daimi,
  month = 	 may,
  note = 	 "38~pp. A revised and numerically much improved
                  version appeared in {\em Annals of Pure and
                  Applied Logic}, 121:1--38, 2003. Extended
                  extended abstract appears in " # ns013 # ",
                  pages 117--122",
  abstract = 	 "In this paper we present another case study in
                  the general project of Proof Mining which means
                  the logical analysis of prima facie
                  non-effective proofs with the aim of extracting
                  new computationally relevant data. We use
                  techniques based on monotone functional
                  interpretation (developed by the first author)
                  to analyze Cheney's simplification from 1965 of
                  Jackson's original proof from 1921 of the
                  uniqueness of the best $L_1$-approximation of
                  continuous functions $f \in C[0,1]$ by
                  polynomials $p\in P_n$ of degree $\leq n$.
                  Cheney's proof is non-effective in the sense
                  that it is based on classical logic and on the
                  non-computational principle WKL (binary
                  K{\"o}nig Lemma). The result of our analysis
                  provides the first effective (in all parameters
                  $f, n$ and $\varepsilon$) uniform modulus of
                  uniqueness (a concept which generalizes `strong
                  uniqueness' studied extensively in
                  approximation theory). Moreover, the extracted
                  modulus has the optimal $\varepsilon
                  $-dependency as follows from Kroo 78. The paper
                  also describes how the uniform modulus of
                  uniqueness can be used to compute the best
                  $L_1$-approximations of a fixed $f \in C[0,1]$
                  with arbitrary precision, and includes some
                  remarks on the case of best Chebycheff
                  approximation",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-13,
  author = 	 "Crazzolara, Federico and Winskel, Glynn",
  title = 	 "Events in Security Protocols",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-13",
  address = 	 daimi,
  month = 	 apr,
  note = 	 "30~pp. Appears in " # acmccs01 # ", pages
                  96--105",
  abstract = 	 "The events of a security protocol and their
                  causal dependency can play an important role in
                  the analysis of security properties. This
                  insight underlies both strand spaces and the
                  inductive method. But neither of these
                  approaches builds up the events of a protocol
                  in a compositional way, so that there is an
                  informal spring from the protocol to its model.
                  By broadening the models to certain kinds of
                  Petri nets, a restricted form of contextual
                  nets, a compositional event-based semantics is
                  given to an economical, but expressive,
                  language for describing security protocols; so
                  the events and dependency of a wide range of
                  protocols are determined once and for all. The
                  net semantics is formally related to a
                  transition semantics, strand spaces and
                  inductive rules, as well as trace languages and
                  event structures, so unifying a range of
                  approaches, as well as providing conditions
                  under which particular, more limited, models
                  are adequate for the analysis of protocols. The
                  net semantics allows the derivation of general
                  properties and proof principles which are
                  demonstrated in establishing an authentication
                  property, following a diagrammatic style of
                  proof",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-12,
  author = 	 "Amtoft, Torben and Consel, Charles and Danvy,
                  Olivier and Malmkj{\ae}r, Karoline",
  title = 	 "The Abstraction and Instantiation of
                  String-Matching Programs",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-12",
  address = 	 daimi,
  month = 	 apr,
  note = 	 "37~pp. Appears in " # lncs2566 # ", pages
                  332--357",
  abstract = 	 "We consider a naive, quadratic string matcher
                  testing whether a pattern occurs in a text, we
                  equip it with a cache mediating its access to
                  the text, and we abstract the traversal policy
                  of the pattern, the cache, and the text. We
                  then specialize this abstracted program with
                  respect to a pattern, using the off-the-shelf
                  partial evaluator Similix.\bibpar
                  Instantiating the abstracted program with a
                  left-to-right traversal policy yields the
                  linear-time behavior of Knuth, Morris and
                  Pratt's string matcher. Instantiating it with a
                  right-to-left policy yields the linear-time
                  behavior of Boyer and Moore's string matcher.",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-11,
  author = 	 "David, Alexandre and M{\"o}ller, M. Oliver",
  title = 	 "From {\sc{HU}ppaal} to {\sc{U}ppaal}: A
                  Translation from Hierarchical Timed Automata to
                  Flat Timed Automata",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-11",
  address = 	 daimi,
  month = 	 mar,
  note = 	 "40~pp. Appears in " # lncs2306 # ", pages
                  218--232, with the title {\em Formal
                  Verification of UML Statecharts with Real-Time
                  Extensions}",
  abstract = 	 "We present a hierarchical version of timed
                  automata, equipped with data types, hand-shake
                  synchronization, and local variables. We
                  describe the formal semantics of this {\em
                  hierarchical timed automata} (HTA) formalism in
                  terms of a transition system.\bibpar
                  We report on the implementation of a flattening
                  algorithm, that translates our formalism to a
                  network of {\sc Uppaal} timed automata. We
                  establish a correspondence between symbolic
                  states of an HTA and its translations, and thus
                  are able to make use of {\sc Uppaal}'s
                  simulator and model checking engine.\bibpar
                  This technique is exemplified with a cardiac
                  pacemaker model. Here, the overhead introduced
                  by the translation is tolerable. We give
                  run-time data for deadlock checking, timed
                  reachability, and timed response analysis",
  linkhtmlabs =  "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-10,
  author = 	 "Fridlender, Daniel and Indrika, Mia",
  title = 	 "Do we Need Dependent Types?",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-10",
  address = 	 daimi,
  month = 	 mar,
  note = 	 "6~pp. Appears in {\em Journal of Functional
                  Programming}, 10(4):409--415, 2000. Superseeds
                  BRICS Report RS-98-38",
  abstract = 	 "Inspired by Danvy, we describe a technique for
                  defining, within the Hindley-Milner type
                  system, some functions which seem to require a
                  language with dependent types. We illustrate
                  this by giving a general definition of {\tt
                  zipWith} for which the Haskell library provides
                  a family of functions, each member of the
                  family having a different type and arity. Our
                  technique consists in introducing ad hoc
                  codings for natural numbers which resemble
                  numerals in $\lambda$-calculus",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}

@techreport{BRICS-RS-01-9,
  author = 	 "Brabrand, Claus and M{\o}ller, Anders and
                  Schwartzbach, Michael I.",
  title = 	 "Static Validation of Dynamically Generated
                  {HTML}",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-9",
  address = 	 daimi,
  month = 	 feb,
  note = 	 "18~pp. Appears in " # acmpaste01 # ", pages
                  38--45",
  abstract = 	 "We describe a static analysis of {\tt}
                  programs that efficiently decides if all
                  dynamically computed XHTML documents presented
                  to the client will validate according to the
                  official DTD. We employ two interprocedural
                  flow analyses to construct a graph summarizing
                  the possible documents. This graph is
                  subsequently analyzed to determine validity of
                  those documents.",
  linkhtmlabs =  "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-8,
  author = 	 "Frendrup, Ulrik and Jensen, Jesper Nyholm",
  title = 	 "Checking for Open Bisimilarity in the $\pi
                  $-Calculus",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-8",
  address = 	 iesd,
  month = 	 feb,
  note = 	 "61~pp",
  abstract = 	 "This paper deals with algorithmic checking of
                  open bisimilarity in the $\pi$-calculus. Most
                  bisimulation checking algorithms are based on
                  the partition refinement approach.
                  Unfortunately the definition of open
                  bisimulation does not permit us to use a
                  partition refinement approach for open
                  bisimulation checking directly, but in the
                  paper \textit{A Partition Refinement Algorithm
                  for the $\pi$-Calculus} Marco Pistore and
                  Davide Sangiogi present an iterative method
                  that makes it possible to check for open
                  bisimilarity using partition refinement. We
                  have implemented the algorithm presented by
                  Marco Pistore and Davide Sangiorgi.
                  Furthermore, we have optimized this algorithm
                  and implemented this optimized algorithm. The
                  time-complexity of this algorithm is the same
                  as the time-complexity for the first algorithm,
                  but performance tests have shown that in many
                  cases the running time of the optimized
                  algorithm is shorter than the running time of
                  the first algorithm. \bibpar
                  Our implementation of the optimized open
                  bisimulation checker algorithm and a user
                  interface have been integrated in a system
                  called the OBC Workbench. The source code and a
                  manual for it is available from
                  \htmladdnormallink
                  {www.cs.auc.dk/research/FS/ny/PR-pi/}{http://www.cs.auc.dk/research/FS/ny/PR-pi/}",
  linkhtmlabs =  "",
  linkps = 	 "",
  linkpdf = 	 ""
}

@techreport{BRICS-RS-01-7,
  author = 	 "Gutin, Gregory and Koh, Khee Meng and Tay, Eng
                  Guan and Yeo, Anders",
  title = 	 "On the Number of Quasi-Kernels in Digraphs",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-7",
  address = 	 daimi,
  month = 	 jan,
  note = 	 "11~pp",
  abstract = 	 "A vertex set $X$ of a digraph $D=(V,A)$ is a
                  {\em kernel} if $X$ is independent (i.e., all
                  pairs of distinct vertices of $X$ are
                  non-adjacent) and for every $v\in V-X$ there
                  exists $x\in X$ such that $vx\in A$. A vertex
                  set $X$ of a digraph $D=(V,A)$ is a {\em
                  quasi-kernel} if $X$ is independent and for
                  every $v\in V-X$ there exist $w\in V-X, x\in X$
                  such that either $vx\in A$ or $vw,wx\in A.$ In
                  1994, Chv{\'a}tal and Lov{\'a}sz proved that
                  every digraph has a quasi-kernel. In 1996,
                  Jacob and Meyniel proved that, if a digraph $D$
                  has no kernel, then $D$ contains at least three
                  quasi-kernels. We characterize digraphs with
                  exactly one and two quasi-kernels, and, thus,
                  provide necessary and sufficient conditions for
                  a digraph to have at least three quasi-kernels.
                  In particular, we prove that every strong
                  digraph of order at least three, which is not a
                  4-cycle, has at least three quasi-kernels. We
                  conjecture that every digraph with no sink has
                  a pair of disjoint quasi-kernels and provide
                  some support to this conjecture",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}

@techreport{BRICS-RS-01-6,
  author = 	 "Gutin, Gregory and Yeo, Anders and Zverovich,
                  Alexey",
  title = 	 "Traveling Salesman Should not be Greedy:
                  Domination Analysis of Greedy-Type Heuristics
                  for the {TSP}",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-6",
  address = 	 daimi,
  month = 	 jan,
  note = 	 "7~pp",
  abstract = 	 "Computational experiments show that the greedy
                  algorithm (GR) and the nearest neighbor
                  algorithm (NN), popular choices for tour
                  construction heuristics, work at acceptable
                  level for the Euclidean TSP, but produce very
                  poor results for the general Symmetric and
                  Asymmetric TSP (STSP and ATSP). We prove that
                  for every $n\ge 2$ there is an instance of ATSP
                  (STSP) on $n$ vertices for which GR finds the
                  worst tour. The same result holds for NN. We
                  also analyze the repetitive NN (RNN) that
                  starts NN from every vertex and chooses the
                  best tour obtained. We prove that, for the
                  ATSP, RNN always produces a tour, which is not
                  worse than at least $n/2-1$ other tours, but
                  for some instance it finds a tour, which is not
                  worse than at most $n-2$ other tours, $n\ge 4$.
                  We also show that, for some instance of the
                  STSP on $n\ge 4$ vertices, RNN produces a tour
                  not worse than at most $2^{n-3}$ tours. These
                  results are in sharp contrast to earlier
                  results by G. Gutin and A. Yeo, and A. Punnen
                  and S. Kabadi, who proved that, for the ATSP,
                  there are tour construction heuristics,
                  including some popular ones, that always build
                  a tour not worse than at least $(n-2)!$ tours",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}

@techreport{BRICS-RS-01-5,
  author = 	 "Hune, Thomas S. and Romijn, Judi and
                  Stoelinga, Mari{\"e}lle and Vaandrager, Frits
                  W.",
  title = 	 "Linear Parametric Model Checking of Timed
                  Automata",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-5",
  address = 	 daimi,
  month = 	 jan,
  note = 	 "44~pp. Appears in " # lncs2031 # ", pages
                  174--188",
  abstract = 	 "We present an extension of the model checker
                  {\sc{U}ppaal} capable of synthesize linear
                  parameter constraints for the correctness of
                  parametric timed automata. The symbolic
                  representation of the (parametric) state-space
                  is shown to be correct. A second contribution
                  of this paper is the identification of a
                  subclass of parametric timed automata (L/U
                  automata), for which the emptiness problem is
                  decidable, contrary to the full class where it
                  is know to be undecidable. Also we present a
                  number of lemmas enabling the verification
                  effort to be reduced for L/U automata in some
                  cases. We illustrate our approach by deriving
                  linear parameter constraints for a number of
                  well-known case studies from the literature
                  (exhibiting a flaw in a published paper)",
  linkhtmlabs =  "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-4,
  author = 	 "Behrmann, Gerd and Fehnker, Ansgar and Hune,
                  Thomas S. and Larsen, Kim G. and Pettersson,
                  Paul and Romijn, Judi",
  title = 	 "Efficient Guiding Towards Cost-Optimality in
                  {\sc{U}ppaal}",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-4",
  address = 	 iesd,
  month = 	 jan,
  note = 	 "21~pp. Appears in " # lncs2031 # ", pages
                  174--188",
  abstract = 	 "In this paper we present an algorithm for
                  efficiently computing the minimum cost of
                  reaching a goal state in the model of Uniformly
                  Priced Timed Automata (UPTA). This model can be
                  seen as a submodel of the recently suggested
                  model of linearly priced timed automata, which
                  extends timed automata with prices on both
                  locations and transitions. The presented
                  algorithm is based on a symbolic semantics of
                  UTPA, and an efficient representation and
                  operations based on difference bound matrices.
                  In analogy with Dijkstra's shortest path
                  algorithm, we show that the search order of the
                  algorithm can be chosen such that the number of
                  symbolic states explored by the algorithm is
                  optimal, in the sense that the number of
                  explored states can not be reduced by any other
                  search order. We also present a number of
                  techniques inspired by branch-and-bound
                  algorithms which can be used for limiting the
                  search space and for quickly finding
                  near-optimal solutions.\bibpar
                  The algorithm has been implemented in the
                  verification tool Uppaal. When applied on a
                  number of experiments the presented techniques
                  reduced the explored state-space with up to
                  90\%",
  linkhtmlabs =  "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-3,
  author = 	 "Behrmann, Gerd and Fehnker, Ansgar and Hune,
                  Thomas S. and Larsen, Kim G. and Pettersson,
                  Paul and Romijn, Judi and Vaandrager, Frits
                  W.",
  title = 	 "Minimum-Cost Reachability for Priced Timed
                  Automata",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-3",
  address = 	 daimi,
  month = 	 jan,
  note = 	 "22~pp. Appears in " # lncs2034 # ", 147--161"
                  ,
  abstract = 	 "This paper introduces the model of linearly
                  priced timed automata as an extension of timed
                  automata, with prices on both transitions and
                  locations. For this model we consider the
                  minimum-cost reachability problem: i.e. given a
                  linearly priced timed automaton and a target
                  state, determine the minimum cost of executions
                  from the initial state to the target state.
                  This problem generalizes the minimum-time
                  reachability problem for ordinary timed
                  automata. We prove decidability of this problem
                  by offering an algorithmic solution, which is
                  based on a combination of branch-and-bound
                  techniques and a new notion of priced regions.
                  The latter allows symbolic representation and
                  manipulation of reachable states together with
                  the cost of reaching them",
  linkhtmlabs =  "",
  linkps = 	 "",
  linkpdf = 	 ""
}

@techreport{BRICS-RS-01-2,
  author = 	 "Pagh, Rasmus and Pagter, Jakob",
  title = 	 "Optimal Time-Space Trade-Offs for
                  Non-Comparison-Based Sorting",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-2",
  address = 	 daimi,
  month = 	 jan,
  note = 	 "ii+20~pp. Appears in " # acmsoda02 # ", pages
                  9--18",
  abstract = 	 "We study the fundamental problem of sorting
                  $n$ integers of $w$ bits on a unit-cost RAM
                  with word size $w$, and in particular consider
                  the time-space trade-off (product of time and
                  space in bits) for this problem. For
                  comparison-based algorithms, the time-space
                  complexity is known to be $\Theta(n^2)$. A
                  result of Beame shows that the lower bound also
                  holds for non-comparison-based algorithms, but
                  no algorithm has met this for time below the
                  comparison-based $\Omega(n\lg n)$ lower
                  bound.\bibpar
                  We show that if sorting within some time bound
                  $\tilde{T}$ is possible, then time $T=O(\tilde
                  {T}+n\lg^* n)$ can be achieved with high
                  probability using space $S=O(n^2/T+w)$, which
                  is optimal. Given a deterministic priority
                  queue using amortized time $t(n)$ per operation
                  and space $n^{O(1)}$, we provide a
                  deterministic algorithm sorting in time
                  $T=O(n\,(t(n) + \lg^* n))$ with $S=O(n^2/T+w)$.
                  Both results require that $w\leq n^{1-\Omega
                  (1)}$. Using existing priority queues and
                  sorting algorithms, this implies that we can
                  deterministically sort time-space optimally in
                  time $\Theta(T)$ for $T\geq n\,(\lg\lg n)^2$,
                  and with high probability for $T\geq n\lg\lg
                  n$.\bibpar
                  Our results imply that recent lower bounds for
                  deciding element distinctness in $o(n\lg n)$
                  time are nearly tight",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}
@techreport{BRICS-RS-01-1,
  author = 	 "Brodal, Gerth St{\o}lting and Fagerberg, Rolf
                  and Pedersen, Christian N. S. and {\"O}stlin,
                  Anna",
  title = 	 "The Complexity of Constructing Evolutionary
                  Trees Using Experiments",
  institution =  brics,
  year = 	 2001,
  type = 	 rs,
  number = 	 "RS-01-1",
  address = 	 daimi,
  month = 	 jan,
  note = 	 "28~pp. Appears in " # lncs2076 # ", pages
                  140--151",
  abstract = 	 "We present a tight upper and lower bound for
                  constructing evolutionary trees using
                  experiments. We present an algorithm which
                  constructs an evolutionary tree of $n$ species
                  using experiments in time $O(n \log_d n)$,
                  where $d$ is the degree of the constructed
                  tree. We show by an explicit adversary argument
                  that any algorithm for constructing an
                  evolutionary tree of $n$ species using
                  experiments must perform $\Omega(n \log_d n)$
                  experiments, where $d$ is the degree of the
                  constructed tree",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
}