@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"}

  author = 	 "Gordon, Andrew D. and Hankin, Paul D. and
                  Lassen, S{\o}ren B.",
  title = 	 "Compilation and Equivalence of Imperative
                  Objects (Revised Report)",
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-55",
  address = 	 daimi,
  month = 	 dec,
  note = 	 "iv+75~pp. This is a revision of Technical
                  Report 429, University of Cambridge Computer
                  Laboratory, June 1997, and the earlier BRICS
                  report \htmladdnormallink
                  {RS-97-19}{http://www.brics.dk/RS/97/19/}, July
                  1997. Appears in {\em Journal of Functional
                  Programming}, 9(4):373-427, 1999, and " #
                  lncs1346 # ", pages 74--87",
  abstract = 	 "We adopt the untyped imperative object
                  calculus of Abadi and Cardelli as a minimal
                  setting in which to study problems of
                  compilation and program equivalence that arise
                  when compiling object-oriented languages. We
                  present both a big-step and a small-step
                  substitution-based operational semantics for
                  the calculus. Our first two results are
                  theorems asserting the equivalence of our
                  substitution-based semantics with a
                  closure-based semantics like that given by
                  Abadi and Cardelli. Our third result is a
                  direct proof of the correctness of compilation
                  to a stack-based abstract machine via a
                  small-step decompilation algorithm. Our fourth
                  result is that contextual equivalence of
                  objects coincides with a form of Mason and
                  Talcott's CIU equivalence; the latter provides
                  a tractable means of establishing operational
                  equivalences. Finally, we prove correct an
                  algorithm, used in our prototype compiler, for
                  statically resolving method offsets. This is
                  the first study of correctness of an
                  object-oriented abstract machine, and of
                  operational equivalence for the imperative
                  object calculus",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
  author = 	 "Danvy, Olivier and Schultz, Ulrik P.",
  title = 	 "Lambda-Dropping: Transforming Recursive
                  Equations into Programs with Block Structure",
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-54",
  address = 	 daimi,
  month = 	 dec,
  note = 	 "55~pp. This report is superseded by the later
                  report \htmladdnormallink{BRICS
  abstract = 	 "Lambda-lifting a block-structured program
                  transforms it into a set of recursive
                  equations. We present the symmetric
                  transformation: lambda-dropping.
                  Lambda-dropping a set of recursive equations
                  restores block structure and lexical
                  For lack of block structure and lexical scope,
                  recursive equations must carry around all the
                  parameters that any of their callees might
                  possibly need. Both lambda-lifting and
                  lambda-dropping thus require one to compute
                  Def/Use paths: 
                  \item for lambda-lifting: each of the functions
                    occurring in the path of a free variable is
                    passed this variable as a parameter; 
                  \item for lambda-dropping: parameters which are
                    used in the same scope as their definition do
                    not need to be passed along in their path. 
                  A program whose blocks have no free variables
                  is scope-insensitive. Its blocks are then free
                  to float (for lambda-lifting) or to sink (for
                  lambda-dropping) along the vertices of the
                  scope tree.\bibpar
                  Our primary application is partial evaluation.
                  Indeed, many partial evaluators for procedural
                  programs operate on recursive equations. To
                  this end, they lambda-lift source programs in a
                  pre-processing phase. But often, partial
                  evaluators [automatically] produce residual
                  recursive equations with dozens of parameters,
                  which most compilers do not handle efficiently.
                  We solve this critical problem by
                  lambda-dropping residual programs in a
                  post-processing phase, which significantly
                  improves both their compile time and their run
                  Lambda-lifting has been presented as an
                  intermediate transformation in compilers for
                  functional languages. We study lambda-lifting
                  and lambda-dropping per se, though
                  lambda-dropping also has a use as an
                  intermediate transformation in a compiler: we
                  noticed that lambda-dropping a program
                  corresponds to transforming it into the
                  functional representation of its optimal SSA
                  form. This observation actually led us to
                  substantially improve our PEPM~'97 presentation
                  of lambda-dropping",
  OPTlinkhtmlabs =  "",
  OPTlinkdvi = 	 "",
  OPTlinkps = 	 "",
  OPTlinkpdf = 	 ""
  author = 	 "Bradfield, Julian C.",
  title = 	 "Fixpoint Alternation: Arithmetic, Transition
                  Systems, and the Binary Tree",
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-53",
  address = 	 daimi,
  month = 	 dec,
  note = 	 "20~pp. Appears in {\em Theoretical Informatics
                  and Applications}, 33:341--356, 1999",
  abstract = 	 "We provide an elementary proof of the fixpoint
                  alternation hierarchy in arithmetic, which in
                  turn allows us to simplify the proof of the
                  modal mu-calculus alternation hierarchy. We
                  further show that the alternation hierarchy on
                  the binary tree is strict, resolving a problem
                  of Niwi{\'n}ski",
  linkhtmlabs =  "",
  linkps = 	 "",
  linkpdf = 	 ""
  author = 	 "Kleist, Josva and Sangiorgi, Davide",
  title = 	 "Imperative Objects and Mobile Processes",
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-52",
  address = 	 iesd,
  month = 	 dec,
  note = 	 "22~pp. Appears in " # ifipprocomet98 # ",
                  pages 285--303",
  abstract = 	 "An interpretation of Abadi and Cardelli's
                  first-order {\em Imperative Object Calculus\/}
                  into a typed $\pi$-calculus is presented. The
                  interpretation validates the subtyping relation
                  and the typing judgements of the Object
                  Calculus, and is computationally adequate. The
                  proof of computational adequacy makes use of (a
                  $\pi$-calculus version) of \emph{ready
                  simulation}, and of a \emph{factorisation} of
                  the interpretation into a functional part and a
                  very simple imperative part. The interpretation
                  can be used to compare and contrast the
                  Imperative and the \emph{Functional} Object
                  Calculi, and to prove properties about them,
                  within a unified framework",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""

  author = 	 "Jensen, Peter Krogsgaard",
  title = 	 "Automated Modeling of Real-Time
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-51",
  address = 	 iesd,
  month = 	 dec,
  note = 	 "9~pp. Appears in " # ieeease98ds # ", pages
  abstract = 	 "This paper describes ongoing work on the
                  automatic construction of formal models from
                  Real-Time implementations. The model
                  construction is based on measurements of the
                  timed behavior of the threads of an
                  implementation, their causal interaction
                  patterns and external visible events. A
                  specification of the timed behavior is modeled
                  in timed automata and checked against the
                  generated model in order to validate their
                  timed behavior",
  linkhtmlabs =  "",
  linkps = 	 "",
  linkpdf = 	 ""
  author = 	 "Aceto, Luca and Ing{\'o}lfsd{\'o}ttir, Anna",
  title = 	 "Testing {Hennessy-Milner} Logic with
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-50",
  address = 	 iesd,
  month = 	 dec,
  note = 	 "15~pp. Appears in " # lncs1578 # ", pages
  abstract = 	 "This study offers a characterization of the
                  collection of properties expressible in
                  Hennessy-Milner Logic (HML) with recursion that
                  can be tested using finite LTSs. In addition to
                  actions used to probe the behaviour of the
                  tested system, the LTSs that we use as tests
                  will be able to perform a distinguished action
                  {\tt nok} to signal their dissatisfaction
                  during the interaction with the tested process.
                  A process $s$ {\sl passes the test} $T$ iff $T$
                  does not perform the action {\tt nok} when it
                  interacts with $s$. A test $T$ tests for a
                  property $\phi$ in HML with recursion iff it is
                  passed by exactly the states that satisfy $\phi
                  $. The paper gives an expressive completeness
                  result offering a characterization of the
                  collection of properties in HML with recursion
                  that are testable in the above sense",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
  author = 	 "Aceto, Luca and Fokkink, Willem Jan and
                  Ing{\'o}lfsd{\'o}ttir, Anna",
  title = 	 "A {Cook's} Tour of Equational Axiomatizations
                  for Prefix Iteration",
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-49",
  address = 	 iesd,
  month = 	 dec,
  note = 	 "14~pp. Appears in " # lncs1378 # ", pages
  abstract = 	 "Prefix iteration is a variation on the
                  original binary version of the Kleene star
                  operation $P^*Q$, obtained by restricting the
                  first argument to be an atomic action, and
                  yields simple iterative behaviours that can be
                  equationally characterized by means of finite
                  collections of axioms. In this paper, we
                  present axiomatic characterizations for a
                  significant fragment of the notions of
                  equivalence and preorder in van Glabbeek's
                  linear-time/branching-time spectrum over
                  Milner's basic CCS extended with prefix
                  iteration. More precisely, we consider ready
                  simulation, simulation, readiness, trace and
                  language semantics, and provide complete
                  (in)equational axiomatizations for each of
                  these notions over BCCS with prefix iteration.
                  All of the axiom systems we present are finite,
                  if so is the set of atomic actions under
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""

  author = 	 "Aceto, Luca and Bouyer, Patricia and
                  Burgue{\~n}o, Augusto and Larsen, Kim G.",
  title = 	 "The Power of Reachability Testing for Timed
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-48",
  address = 	 iesd,
  month = 	 dec,
  note = 	 "12~pp. Appears in " # lncs1530 # ", pages
  abstract = 	 "In this paper we provide a complete
                  characterization of the class of properties of
                  (networks of) timed automata for which model
                  checking can be reduced to reachability
                  checking in the context of testing automata",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""

  author = 	 "Behrmann, Gerd and Larsen, Kim G. and Pearson,
                  Justin and Weise, Carsten and Yi, Wang",
  title = 	 "Efficient Timed Reachability Analysis using
                  Clock Difference Diagrams",
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-47",
  address = 	 iesd,
  month = 	 dec,
  note = 	 "13~pp. Appears in " # lncs1633 # ", pages
  abstract = 	 "One of the major problems in applying
                  automatic verification tools to industrial-size
                  systems is the excessive amount of memory
                  required during the state-space exploration of
                  a model. In the setting of real-time, this
                  problem of state-explosion requires extra
                  attention as information must be kept not only
                  on the discrete control structure but also on
                  the values of continuous clock
                  In this paper, we present Clock Difference
                  Diagrams, CDD's, a BDD-like data-structure for
                  representing and effectively manipulating
                  certain non-convex subsets of the Euclidean
                  space, notably those encountered during
                  verification of timed automata.\bibpar
                  A version of the real-time verification tool
                  {\sc Uppaal} using CDD's as a compact
                  data-structure for storing explored symbolic
                  states has been implemented. Our experimental
                  results demonstrate significant space-savings:
                  for 8 industrial examples, the savings are
                  between 46\% and 99\% with moderate increase in
                  We further report on how the symbolic
                  state-space exploration itself may be carried
                  out using CDD's",
  linkhtmlabs =  "",
  linkps = 	 "",
  linkpdf = 	 ""
  author = 	 "Larsen, Kim G. and Weise, Carsten and Yi, Wang
                  and Pearson, Justin",
  title = 	 "Clock Difference Diagrams",
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-46",
  address = 	 iesd,
  month = 	 dec,
  note = 	 "18~pp. Presented at " # nwpt10 # ". Appears in
                  {\em Nordic Journal of Computing},
                  6(3):271--298, 1999",
  abstract = 	 "We sketch a BDD-like structure for
                  representing unions of simple convex polyhedra,
                  describing the legal values of a set of clocks
                  given bounds on the values of clocks and clock
  linkhtmlabs =  "",
  linkps = 	 "",
  linkpdf = 	 ""
  author = 	 "Jensen, Morten Vadsk{\ae}r and Nielsen,
  title = 	 "Real-Time Layered Video Compression using
                  {SIMD} Computation",
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-45",
  address = 	 daimi,
  month = 	 dec,
  note = 	 "37~pp. Appears in " # lncs1557 # ", pages
  abstract = 	 "We present the design and implementation of a
                  high performance layered vi\-de\-o co\-dec,
                  designed for deployment in bandwidth
                  heterogeneous networks. The codec combines
                  wavelet based subband decomposition and
                  discrete cosine transforms to facilitate
                  layered spatial and SNR (signal-to-noise ratio)
                  coding for bit-rate adaption to a wide range of
                  receiver capabilities. We show how a test video
                  stream can be partitioned into several distinct
                  layers of increasing visual quality and
                  bandwidth requirements, with the difference
                  between highest and lowest requirement being
                  Through the use of the Visual Instruction Set
                  on SUN's UltraSPARC platform we demonstrate how
                  SIMD parallel image processing enables
                  real-time layered encoding and decoding in
                  software. Our $384\times 320\times 24$-bit test
                  video stream is partitioned into 21 layers at a
                  speed of 39 frames per second and reconstructed
                  at 28 frames per second. Our VIS accelerated
                  encoder stages are about 3-4 times as fast as
                  an optimized C version. We find that this
                  speedup is well worth the extra implementation
  linkhtmlabs =  "",
  linkps = 	 "",
  linkpdf = 	 ""

  author = 	 "Nielsen, Brian and Agha, Gul",
  title = 	 "Towards Re-usable Real-Time Objects",
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-44",
  address = 	 iesd,
  month = 	 dec,
  note = 	 "36~pp. Appears in {\em The Annals of Software
                  Engineering}, 7:257--282, 1999",
  abstract = 	 "Large and complex real-time systems can
                  benefit significantly from a component-based
                  development approach where new systems are
                  constructed by composing reusable, documented
                  and previously tested concurrent objects.
                  However, reusing objects which execute under
                  real-time constraints is problematic because
                  application specific time and synchronization
                  constraints are often embedded in the internals
                  of these objects. The tight coupling of
                  functionality and real-time constraints makes
                  objects interdependent, and as a result
                  difficult to reuse in another system.\bibpar
                  We propose a model which facilitates separate
                  and modular specification of real-time
                  constraints, and show how separation of
                  real-time constraints and functional behavior
                  is possible. We present our ideas using the
                  {\it Actor model} to represent untimed objects,
                  and the {\it Real-time Synchronizers} language
                  to express real-time and synchronization
                  constraints. We discuss specific mechanisms by
                  which {\it Real-time Synchronizers} can govern
                  the interaction and execution of untimed
                  We treat our model formally, and succinctly
                  define what effect real-time constraints have
                  on a set of concurrent objects. We briefly
                  discuss how a middleware scheduling and
                  event-dispatching service can use the
                  synchronizers to execute the system",
  linkhtmlabs =  "",
  linkps = 	 "",
  linkpdf = 	 ""
  author = 	 "Mosses, Peter D.",
  title = 	 "{CASL}: A Guided Tour of its Design",
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-43",
  address = 	 daimi,
  month = 	 dec,
  note = 	 "31~pp. Appears in " # lncs1589 # ", pages
  abstract = 	 "{\sc Casl} is an expressive language for the
                  specification of functional requirements and
                  modular design of software. It has been
                  designed by {\sc CoFI}, the international
                  Common Framework Initiative for algebraic
                  specification and development. It is based on a
                  critical selection of features that have
                  already been explored in various contexts,
                  including subsorts, partial functions,
                  first-order logic, and structured and
                  architectural specifications. {\sc Casl} should
                  facilitate interoperability of many existing
                  algebraic prototyping and verification
                  This guided tour of the {\sc Casl} design is
                  based closely on a 1/2-day tutorial held at
                  ETAPS~'98 (corresponding slides are available
                  from the {\sc CoFI} archives). The major issues
                  that had to be resolved in the design process
                  are indicated, and all the main concepts and
                  constructs of {\sc Casl} are briefly explained
                  and illustrated---the reader is referred to the
                  {\sc Casl} Language Summary for further
                  details. Some familiarity with the fundamental
                  concepts of algebraic specification would be
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
  author = 	 "Mosses, Peter D.",
  title = 	 "Semantics, Modularity, and Rewriting Logic",
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-42",
  address = 	 daimi,
  month = 	 dec,
  note = 	 "20~pp. Appears in " # entcs15,
  abstract = 	 "A complete formal semantic description of a
                  practical programming language (such as Java)
                  is likely to be a lengthy document, regardless
                  of which semantic framework is being used. Good
                  modularity of the description is important to
                  the person(s) developing it, to facilitate
                  reuse, change, and extension. Unfortunately,
                  the conventional versions of the major semantic
                  frameworks have rather poor modularity.\bibpar
                  In this paper, we first recall some approaches
                  that improve the modularity of denotational
                  semantics, namely \emph{action semantics},
                  \emph{modular monadic semantics}, and a hybrid
                  framework that combines these: \emph{modular
                  monadic action semantics}. We then address the
                  issue of modularity in \emph{operational
                  semantics}, which appears to have received
                  comparatively little attention so far, and
                  report on some preliminary investigations of
                  how one might achieve the same kind of
                  modularity in structural operational semantics
                  as the use of monad transformers can provide in
                  denotational semantics---this is the main
                  technical contribution of the paper. Finally,
                  we briefly consider the representation of
                  structural operational semantics in rewriting
                  logic, and speculate on the possibility of
                  using it to interpret programs in the described
                  language. Providing powerful meta-tools for
                  such semantics-based interpretation is an
                  interesting potential application of rewriting
                  logic; good modularity of the semantic
                  descriptions may be crucial for the
                  practicality of using the tools.\bibpar
                  Much of the paper consists of (very) simple
                  examples of semantic descriptions in the
                  various frameworks, illustrating the degree of
                  reformulation needed when extending the
                  described language---a strong indicator of
                  modularity. Throughout, it is assumed that the
                  reader has some familiarity with the concepts
                  and notation of denotational and structural
                  operational semantics. Familiarity with the
                  basic notions of monads and monad transformers
                  is not a prerequisite",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""

  author = 	 "Kohlenbach, Ulrich",
  title = 	 "The Computational Strength of Extensions of
                  Weak {K}{\"o}nig's Lemma",
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-41",
  address = 	 daimi,
  month = 	 dec,
  note = 	 "23~pp",
  abstract = 	 "The weak K{\"o}nig's lemma WKL is of crucial
                  significance in the study of fragments of
                  mathematics which on the one hand are
                  mathematically strong but on the other hand
                  have a low proof-theoretic and computational
                  strength. In addition to the restriction to
                  binary trees (or equivalently bounded trees),
                  WKL is also `weak' in that the tree predicate
                  is quantifier-free. Whereas in general the
                  computational and proof-theoretic strength
                  increases when logically more complex trees are
                  allowed, we show that this is not the case for
                  trees which are given by formulas in a class
                  $\Phi_{\infty}$ where we allow an arbitrary
                  function quantifier prefix over bounded
                  functions in front of a $\Pi^0_1$-formula. This
                  results in a schema $\Phi_{\infty}$-WKL. \\
                  Another way of looking at WKL is via its
                  equivalence to the principle \[ \forall
                  x\exists y\le 1 \forall z\,
                  A_0(x,y,z)\rightarrow\exists f\le\lambda
                  x.1\forall x,z \, A_0(x,fx,z), \] where $A_0$
                  is a quantifier-free formula ($x,y,z$ are
                  natural number variables). We generalize this
                  to $\Phi_{\infty}$-formulas as well and allow
                  function quantifiers `$\exists g\le s$' instead
                  of `$\exists y\le 1$', where $g\le s$ is
                  defined pointwise. The resulting schema is
                  called $\Phi_{\infty}$-b-AC$^{0,1}$.\\
                  In the absence of functional parameters (so in
                  particular in a second order context), the
                  corresponding versions of $\Phi_{\infty}$-WKL
                  and $\Phi_{\infty}$-b-AC$^{0,1}$ turn out to be
                  equivalent to WKL. This changes completely in
                  the presence of functional variables of type
                  $2$ where we get proper hierarchies of
                  principles $\Phi_n$-WKL and $\Phi_n
                  $-b-AC$^{0,1}$. Variables of type $2$ however
                  are necessary for a direct representation of
                  analytical objects and -- sometimes -- for a
                  faithful representation of such objects at all
                  as we will show in a subsequent paper. By a
                  reduction of $\Phi_{\infty}$-WKL and $\Phi_
                  {\infty}$-b-AC$^{0,1}$ to a non-standard axiom
                  $F$ (introduced in a previous paper) and a new
                  elimination result for $F$ relative to various
                  fragment of arithmetic in all finite types, we
                  prove that $\Phi_{\infty}$-WKL and $\Phi_
                  {\infty}$-b-AC$^{0,1}$ do neither contribute to
                  the provably recursive functionals of these
                  fragments nor to their proof-theoretic
                  strength. In a subsequent paper we will
                  illustrate the greater mathematical strength of
                  these principles (compared to WKL)",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""

  author = 	 "Andersen, Henrik Reif and Stirling, Colin and
                  Winskel, Glynn",
  title = 	 "A Compositional Proof System for the Modal
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-40",
  address = 	 daimi,
  month = 	 dec,
  note = 	 "29~pp. Extended abstract appears in " # lics9
                  # ", pages 144--153. Superseeds the earlier
                  BRICS Report RS-94-34",
  abstract = 	 "We present a proof system for determining
                  satisfaction between processes in a fairly
                  general process algebra and assertions of the
                  modal $\mu$-calculus. The proof system is
                  compositional in the structure of processes. It
                  extends earlier work on compositional reasoning
                  within the modal $\mu$-calculus and combines it
                  with techniques from work on local model
                  checking. The proof system is sound for all
                  processes and complete for a class of
                  finite-state processes",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
  author = 	 "Fridlender, Daniel",
  title = 	 "An Interpretation of the {F}an Theorem in Type
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-39",
  address = 	 daimi,
  month = 	 dec,
  note = 	 "15~pp. Appears in " # lncs1657 # ", pages
  abstract = 	 "This article presents a formulation of the fan
                  theorem in Martin-L{\"o}f's type theory.
                  Starting from one of the standard versions of
                  the fan theorem we gradually introduce
                  reformulations leading to a final version which
                  is easy to interpret in type theory. Finally we
                  describe a formal proof of that final version
                  of the fan theorem",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
  author = 	 "Fridlender, Daniel and Indrika, Mia",
  title = 	 "An $n$-ary {\tt zipWith} in {H}askell",
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-38",
  address = 	 daimi,
  month = 	 dec,
  note = 	 "12~pp",
  abstract = 	 "The aim of this note is to present an
                  alternative definition of the {\tt zipWith}
                  family in the Haskell Library Report. Because
                  of the difficulties in defining a well-typed
                  function with a variable number of arguments,
                  the library presents a family of {\tt zipWith}
                  functions. It provides zip functions ${\tt
                  zipWith}_2, {\tt zipWith}_3, \ldots, {\tt
                  zipWith}_7$. For each $n$, ${\tt zipWith}_n$
                  zips $n$ lists with a $n$-ary function.
                  Defining a single {\tt zipWith} function with a
                  variable number of arguments seems to require
                  dependent types. We show, however, how to
                  define such a function in Haskell by means of a
                  binary operator for grouping its arguments. For
                  comparison, we also give definitions of {\tt
                  zipWith} in languages with dependent types",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""

  author = 	 "Damg{\aa}rd, Ivan B. and Kilian, Joe and
                  Salvail, Louis",
  title = 	 "On the (Im)possibility of Basing Oblivious
                  Transfer and Bit Commitment on Weakened
                  Security Assumptions",
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-37",
  address = 	 daimi,
  month = 	 dec,
  note = 	 "22~pp. Appears in " # lncs1592 # ", pages
  abstract = 	 "We consider the problem of basing Oblivious
                  Transfer (OT) and Bit Commitment (BC), with
                  information theoretic security, on seemingly
                  weaker primitives. We introduce a general model
                  for describing such primitives, called {\em
                  Weak Generic Transfer} (WGT). This model
                  includes as important special cases {\em Weak
                  Oblivious Transfer} (WOT), where both the
                  sender and receiver may learn too much about
                  the other party's input, and a new, more
                  realistic model of noisy channels, called {\em
                  unfair noisy channels}. An unfair noisy channel
                  has a known range of possible noise levels;
                  protocols must work for any level within this
                  range against adversaries who know the actual
                  noise level.\bibpar
                  We give a precise characterization for when one
                  can base OT on WOT. When the deviation of the
                  WOT from the ideal is above a certain
                  threshold, we show that no
                  information-theoretic reductions from OT (even
                  against passive adversaries) and BC exist; when
                  the deviation is below this threshold, we give
                  a reduction from OT (and hence BC) that is
                  information-theoretically secure against active
                  For unfair noisy channels we show a similar
                  threshold phenomenon for bit commitment. If the
                  upper bound on the noise is above a threshold
                  (given as function of the lower bound) then no
                  information-theoretic reduction from OT (even
                  against passive adversaries) or BC exist; when
                  it is below this threshold we give a reduction
                  from BC. As a partial result, we give a
                  reduction from OT to UNC for smaller noise
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
  author = 	 "Cramer, Ronald and Damg{\aa}rd, Ivan B. and
                  Dziembowski, Stefan and Hirt, Martin and Rabin,
  title = 	 "Efficient Multiparty Computations with
                  Dishonest Minority",
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-36",
  address = 	 daimi,
  month = 	 dec,
  note = 	 "19~pp. Appears in " # lncs1592 # ", pages
  abstract = 	 "We consider verifiable secret sharing (VSS)
                  and multiparty computation (MPC) in the secure
                  channels model, where a broadcast channel is
                  given and a non-zero error probability is
                  allowed. In this model Rabin and Ben-Or
                  proposed VSS and MPC protocols, secure against
                  an adversary that can corrupt any minority of
                  the players. In this paper, we first observe
                  that a subprotocol of theirs, known as weak
                  secret sharing (WSS), is not secure against an
                  adaptive adversary, contrary to what was
                  believed earlier. We then propose new and
                  adaptively secure protocols for WSS, VSS and
                  MPC that are substantially more efficient than
                  the original ones. Our protocols generalize
                  easily to provide security against general
                  $Q^2$ adversaries",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
  author = 	 "Danvy, Olivier and Yang, Zhe",
  title = 	 "An Operational Investigation of the {CPS}
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-35",
  address = 	 daimi,
  month = 	 dec,
  note = 	 "Extended version of a paper appearing in " #
                  LNCS1576 # ", pages 224--242",
  abstract = 	 "We explore the hierarchy of control induced by
                  successive transformations into
                  continuation-passing style (CPS) in the
                  presence of ``control delimiters'' and
                  ``composable continuations''. Specifically, we
                  investigate the structural operational
                  semantics associated with the CPS
                  To this end, we characterize an operational
                  notion of continuation semantics. We relate it
                  to the traditional CPS transformation and we
                  use it to account for the control operator
                  shift and the control delimiter reset
                  operationally. We then transcribe the resulting
                  continuation semantics in ML, thus obtaining a
                  native and modular implementation of the entire
                  hierarchy. We illustrate it with a few
                  examples, the most significant of which is
                  layered monads",
  linkhtmlabs =  ""
  author = 	 "Binderup, Peter G. and Frandsen, Gudmund
                  Skovbjerg and Miltersen, Peter Bro and Skyum,
  title = 	 "The Complexity of Identifying Large
                  Equivalence Classes",
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-34",
  address = 	 daimi,
  month = 	 dec,
  note = 	 "Appears in {\em Fundamenta Informaticae},
  abstract = 	 "We prove that at least $\frac{3k-4}{k(2k-3)}{n
                  \choose 2}-{\rm O}(k)$ equivalence tests and no
                  more than $\frac{2}{k}{n\choose 2}+{\rm O}(n)$
                  equivalence tests are needed in the worst case
                  to identify the equivalence classes with at
                  least $k$ members in set of $n$ elements. The
                  upper bound is an improvement by a factor 2
                  compared to known results. For $k=3$ we give
                  tighter bounds. Finally, for $k > \frac{n}{2}$
                  we prove that it is necessary and it suffices
                  to make $2n-k-1$ equivalence tests which
                  generalizes a known result for $k=\lceil\frac
                  {n+1}{2} \rceil$",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
  author = 	 "H{\"u}ttel, Hans and Kleist, Josva and
                  Nestmann, Uwe and Merro, Massimo",
  title = 	 "Migration = Cloning ; Aliasing (Preliminary
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-33",
  address = 	 iesd,
  month = 	 dec,
  note = 	 "40~pp. Appears in " # fool6,
  abstract = 	 "In Obliq, a lexically scoped, distributed,
                  object-based programming language, object
                  migration was suggested as creating a (remote)
                  copy of an object's state at the target site,
                  followed by turning the (local) object itself
                  into an alias, also called \emph{surrogate},
                  for the just created remote copy.\bibpar
                  We consider the creation of object surrogates
                  as an abstraction of the above-mentioned style
                  of migration. We introduce {\O}jeblik, a
                  distribution-free subset of Obliq, and provide
                  two formal semantics, one in an intuitive
                  configuration style, the other in terms of a
                  pi-calculus. The intuitive semantics shows why
                  surrogation is neither safe in Obliq, nor can
                  it be so in full generality in Repliq (a
                  repaired Obliq). The pi-calculus semantics
                  allows us to prove that surrogation in
                  {\O}jeblik is safe for certain well-identified
                  cases, thus suggesting that migration in Repliq
                  may be safe, accordingly",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
  author = 	 "Camenisch, Jan and Damg{\aa}rd, Ivan B.",
  title = 	 "Verifiable Encryption and Applications to
                  Group Signatures and Signature Sharing",
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-32",
  address = 	 daimi,
  month = 	 dec,
  note = 	 "18~pp. Appears in " # lncs1976 # ", pages
  abstract = 	 "We generalise and improve the security and
                  efficiency of the verifiable encryption scheme
                  of Asokan et al., such that it can rely on more
                  general assumptions, and can be proven secure
                  without relying on random oracles. We show a
                  new application of verifiable encryption to
                  group signatures with separability, these
                  schemes do not need special purpose keys but
                  can work with a wide range of signature and
                  encryption schemes already in use. Finally, we
                  extend our basic primitive to verifiable
                  threshold and group encryption. By encrypting
                  digital signatures this way, one gets new
                  solutions to the verifiable signature sharing
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
  author = 	 "Winskel, Glynn",
  title = 	 "A Linear Metalanguage for Concurrency",
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-31",
  address = 	 daimi,
  month = 	 nov,
  note = 	 "21~pp. Appears in " # lncs1548 # ", pages
  abstract = 	 "A metalanguage for concurrent process
                  languages is introduced. Within it a range of
                  process languages can be defined, including
                  higher-order process languages where processes
                  are passed and received as arguments. (The
                  process language has, however, to be linear, in
                  the sense that a process received as an
                  argument can be run at most once, and not
                  include name generation as in the Pi-Calculus.)
                  The metalanguage is provided with two
                  interpretations both of which can be understood
                  as categorical models of a variant of linear
                  logic. One interpretation is in a simple
                  category of nondeterministic domains; here a
                  process will denote its set of traces. The
                  other interpretation, obtained by direct
                  analogy with the nondeterministic domains, is
                  in a category of presheaf categories; the
                  nondeterministic branching behaviour of a
                  process is captured in its denotation as a
                  presheaf. Every presheaf category possesses a
                  notion of (open-map) bisimulation, preserved by
                  terms of the metalanguage. The conclusion
                  summarises open problems and lines of future
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
  author = 	 "Butz, Carsten",
  title = 	 "Finitely Presented {H}eyting Algebras",
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-30",
  address = 	 daimi,
  month = 	 nov,
  note = 	 "30~pp",
  abstract = 	 "In this paper we study the structure of
                  finitely presented Heyting algebras. Using
                  algebraic techniques (as opposed to techniques
                  from proof-theory) we show that every such
                  Heyting algebra is in fact co-Heyting,
                  improving on a result of Ghilardi who showed
                  that Heyting algebras free on a finite set of
                  generators are co-Heyting. Along the way we
                  give a new and simple proof of the finite model
                  Our main technical tool is a representation of
                  finitely presented Heyting algebras in terms of
                  a colimit of finite distributive lattices. As
                  applications we construct explicitly the
                  minimal join-irreducible elements (the atoms)
                  and the maximal join-irreducible elements of a
                  finitely presented Heyting algebras in terms of
                  a given presentation. This gives as well a new
                  proof of the disjunction property for
                  intuitionistic propositional logic",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""

  author = 	 "Camenisch, Jan and Michels, Markus",
  title = 	 "Proving in Zero-Knowledge that a Number is the
                  Product of Two Safe Primes",
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-29",
  address = 	 daimi,
  month = 	 nov,
  note = 	 "19~pp. Appears in " # lncs1592 # ", pages
  abstract = 	 "
                  This paper presents the first efficient
                  statistical zero-knowledge protocols to prove
                  statements such as:
                  \item A committed number is a pseudo-prime. 
                  \item A committed (or revealed) number is the
                    product of two safe primes, i.e., primes $p$
                    and $q$ such that $(p-1)/2$ and $(q-1)/2$ are
                    primes as well. 
                  \item A given value is of large order modulo a
                    composite number that consists of two safe
                    prime factors. 
                  So far, no methods other than inefficient
                  circuit-based proofs are known for proving such
                  properties. Proving the second property is for
                  instance necessary in many recent cryptographic
                  schemes that rely on both the hardness of
                  computing discrete logarithms and of difficulty
                  computing roots modulo a composite.\bibpar
                  The main building blocks of our protocols are
                  statistical zero-knowledge proofs that are of
                  independent interest. Mainly, we show how to
                  prove the correct computation of a modular
                  addition, a modular multiplication, or a
                  modular exponentiation, where all values
                  including the modulus are committed but {\em
                  not}\/ publicly known. Apart from the validity
                  of the computation, no other information about
                  the modulus (e.g., a generator which order
                  equals the modulus) or any other operand is
                  given. Our technique can be generalized to
                  prove in zero-knowledge that any multivariate
                  polynomial equation modulo a certain modulus is
                  satisfied, where only commitments to the
                  variables of the polynomial and a commitment to
                  the modulus must be known. This improves
                  previous results, where the modulus is publicly
                  We show how a prover can use these building
                  blocks to convince a verifier that a committed
                  number is prime. This finally leads to
                  efficient protocols for proving that a
                  committed (or revealed) number is the product
                  of two safe primes. As a consequence, it can be
                  shown that a given value is of large order
                  modulo a given number that is a product of two
                  safe primes.
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
  author = 	 "Pagh, Rasmus",
  title = 	 "Low Redundancy in Dictionaries with {$O(1)$}
                  Worst Case Lookup Time",
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-28",
  address = 	 daimi,
  month = 	 nov,
  note = 	 "15~pp. Journal version in {\em SIAM Journal on
                  Computing} 31:353--363, 2001, and proceedings
                  version in " # lncs1644 # ", pages 595--604",
  abstract = 	 "A {\it static dictionary} is a data structure
                  for storing subsets of a finite universe $U$,
                  so that membership queries can be answered
                  efficiently. We study this problem in a unit
                  cost RAM model with word size $\Omega(\log
                  |U|)$, and show that for $n$-element subsets,
                  constant worst case query time can be obtained
                  using $B+O(\log\log|U|)+o(n)$ bits of storage,
                  where $B=\lceil\log_2{{|U|}\choose{n}} \rceil$
                  is the minimum number of bits needed to
                  represent all such subsets. The solution for
                  dense subsets uses $B+O(\frac{|U|\log\log
                  |U|}{\log|U|})$ bits of storage, and supports
                  constant time rank queries. In a dynamic
                  setting, allowing insertions and deletions, our
                  techniques give an $O(B)$ bit space usage",
  linkhtmlabs =  "",
  linkps = 	 "",
  linkpdf = 	 ""
  author = 	 "Camenisch, Jan and Michels, Markus",
  title = 	 "A Group Signature Scheme Based on an
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-27",
  address = 	 daimi,
  month = 	 nov,
  note = 	 "18~pp. Preliminary version appeared in " #
                  lncs1514 # ", pages 160--174",
  keywords = 	 "Group signature scheme for large groups,
                  digital signature scheme, revocable anonymity",
  abstract = 	 "The concept of group signatures allows a group
                  member to sign messages anonymously on behalf
                  of the group. However, in the case of a
                  dispute, the identity of a signature's
                  originator can be revealed by a designated
                  entity. In this paper we propose a new group
                  signature scheme that is well suited for large
                  groups, i.e., the length of the group's public
                  key and of signatures do not depend on the size
                  of the group. Our scheme is based on a
                  variation of the RSA problem called strong RSA
                  assumption. It is also more efficient than
                  previous ones satisfying these requirements",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""

  author = 	 "Quaglia, Paola and Walker, David",
  title = 	 "On Encoding $p\pi$ in $m\pi$",
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-26",
  address = 	 daimi,
  month = 	 oct,
  note = 	 "27 pp. Full version of paper appearing in " #
                  lncs1530 # ", pages 42--53",
  abstract = 	 "This paper is about the encoding of $p\pi$,
                  the polyadic $\pi$-calculus, in $m\pi$, the
                  monadic $\pi$-calculus. A type system for $m\pi
                  $ processes is introduced that captures the
                  interaction regime underlying the encoding of
                  $p\pi$ processes respecting a sorting. A
                  full-abstraction result is shown: two $p\pi$
                  processes are typed barbed congruent iff their
                  $m\pi$ encodings are monadic-typed barbed
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
  author = 	 "Dubhashi, Devdatt P.",
  title = 	 "{T}alagrand's Inequality in Hereditary
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-25",
  address = 	 daimi,
  month = 	 oct,
  note = 	 "22~pp",
  abstract = 	 "We develop a nicely packaged form of
                  Talagrand's inequality that can be applied to
                  prove concentration of measure for functions
                  defined by hereditary properties. We illustrate
                  the framework with several applications from
                  combinatorics and algorithms. We also give an
                  extension of the inequality valid in spaces
                  satisfying a certain negative dependence
                  property and give some applications",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
  author = 	 "Dubhashi, Devdatt P.",
  title = 	 "{T}alagrand's Inequality and Locality in
                  Distributed Computing",
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-24",
  address = 	 daimi,
  month = 	 oct,
  note = 	 "14~pp Appears in " # lncs1518 # ", pages
  abstract = 	 "We illustrate the use of Talagrand's
                  inequality and an extension of it to dependent
                  random variables due to Marton for the analysis
                  of distributed randomised algorithms,
                  specifically, for edge colouring graphs",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
  author = 	 "Dubhashi, Devdatt P.",
  title = 	 "Martingales and Locality in Distributed
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-23",
  address = 	 daimi,
  month = 	 oct,
  note = 	 "19~pp. Appears in " # lncs1530 # ", pages
  abstract = 	 "We use Martingale inequalities to give a
                  simple and uniform analysis of two families of
                  distributed randomised algorithms for edge
                  colouring graphs",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
  author = 	 "Cattani, Gian Luca and Power, John and
                  Winskel, Glynn",
  title = 	 "A Categorical Axiomatics for Bisimulation",
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-22",
  address = 	 daimi,
  month = 	 sep,
  note = 	 "ii+21~pp. Appears in " # lncs1466 # ", pages
  abstract = 	 "We give an axiomatic category theoretic
                  account of bisimulation in process algebras
                  based on the idea of functional bisimulations
                  as open maps. We work with 2-monads, $T$, on
                  {\bf Cat}. Operations on processes, such as
                  nondeterministic sum, prefixing and parallel
                  composition are modelled using functors in the
                  Kleisli category for the 2-monad $T$. We may
                  define the notion of open map for any such
                  2-monad; in examples of interest, that agrees
                  exactly with the usual notion of functional
                  bisimulation. Under a condition on $T$, namely
                  that it be a dense $KZ$-monad, which we define,
                  it follows that functors in $Kl(T)$ preserve
                  open maps, i.e., they respect functional
                  bisimulation. We further investigate structures
                  on $Kl(T)$ that exist for axiomatic reasons,
                  primarily because $T$ is a dense $KZ$-monad,
                  and we study how those structures help to model
                  operations on processes. We outline how this
                  analysis gives ideas for modelling higher order
                  processes. We conclude by making comparison
                  with the use of presheaves and profunctors to
                  model process calculi",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""

  author = 	 "Power, John and Cattani, Gian Luca and
                  Winskel, Glynn",
  title = 	 "A Representation Result for Free
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-21",
  address = 	 daimi,
  month = 	 sep,
  note = 	 "16~pp. Appears in {\em Journal of Pure and
                  Applied Algebra}, 151(3):273--286 (2000)",
  abstract = 	 "Given a class $F$ of weights, one can consider
                  the construction that takes a small category
                  $C$ to the free cocompletion of $C$ under
                  weighted colimits, for which the weight lies in
                  $F$. Provided these free $F$-cocompletions are
                  small, this construction generates a $2$-monad
                  on {\bf Cat}, or more generally on $V$-${\bf
                  Cat}$ for monoidal biclosed complete and
                  cocomplete $V$. We develop the notion of a
                  dense $2$-monad on $V$-{\bf Cat} and
                  characterise free $F$-cocompletions by dense
                  $KZ$-monads on $V$-{\bf Cat}. We prove various
                  corollaries about the structure of such
                  $2$-monads and their Kleisli $2$-categories, as
                  needed for the use of open maps in giving an
                  axiomatic study of bisimulation in concurrency.
                  This requires the introduction of the concept
                  of a pseudo-commutativity for a strong
                  $2$-monad on a symmetric monoidal $2$-category,
                  and a characterisation of it in terms of
                  structure on the Kleisli $2$-category",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 "",
  linkpdf = 	 ""
  author = 	 "Riis, S{\o}ren and Sitharam, Meera",
  title = 	 "Uniformly Generated Submodules of Permutation
  institution =  brics,
  year = 	 1998,
  type = 	 rs,
  number = 	 "RS-98-20",
  address = 	 daimi,
  month = 	 sep,
  note = 	 "35~pp. Appears in {\em Annals of Pure and
                  Applied Algebra}, 160(3):285--318, 2001",
  abstract = 	 "This paper is motivated by a link between
                  algebraic proof complexity and the
                  representation theory of the finite symmetric
                  groups. Our perspective leads to a series of
                  non-traditional problems in the representation
                  theory of $S_n$.\bibpar
                  Most of our technical results concern the
                  structure of ``uniformly'' generated submodules
                  of permutation modules. We consider (for
                  example) sequences $W_n$ of submodules of the
                  permutation modules $M^{(n-k,1^k)}$ and prove
                  that if the modules $W_n$ are given in a
                  uniform way - which we make precise - the
                  dimension $p(n)$ of $W_n$ (as a vector space)
                  is a single polynomial with rational
                  coefficients, for all but finitely many
                  ``singular'' values of $n$. Furthermore, we
                  show that ${\rm dim}(W_n)