@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 = 	 "Godskesen, Jens Chr{.} and Larsen, Kim G.",
  title = 	 "Synthesizing Distinguishing Formulae for Real
                  Time Systems",
  institution =  brics,
  year = 	 1994,
  type = 	 rs,
  number = 	 "RS-94-48",
  address = 	 iesd,
  month = 	 dec,
  note = 	 "21~pp. Extended abstract appears in " #
                  lncs969 # ", pages 519--528",
  abstract = 	 "This paper describes a technique for
                  generating diagnostic information for the {\sl
                  timed} bisimulation equivalence and the {\sl
                  timed} simulation preorder. More precisely,
                  given two (parallel) networks of regular
                  real--time processes, the technique will
                  provide a logical formula that differentiates
                  them in case they are not timed (bi)similar.
                  Our method may be seen as an extension of the
                  algorithm by {\v C}er{\=a}ns for deciding timed
                  bisimilarity in that information of
                  time--quantities has been added sufficient for
                  generating distinguishing formulae. The
                  technique has been added to the automatic
                  verification tool {\sc Epsilon} and applied to
                  various examples.",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 ""
  author = 	 "Larsen, Kim G. and Steffen, Bernhard and
                  Weise, Carsten",
  title = 	 "A Constraint Oriented Proof Methodology based
                  on Modal Transition Systems",
  institution =  brics,
  year = 	 1994,
  type = 	 rs,
  number = 	 "RS-94-47",
  address = 	 iesd,
  month = 	 dec,
  note = 	 "13 pp",
  abstract = 	 "In this paper, we present a
                  constraint-oriented state-based proof
                  methodology for concurrent software systems
                  which exploits compositionality and abstraction
                  for the reduction of the verification problem
                  under investigation. Formal basis for this
                  methodology are Modal Transition Systems
                  allowing loose state-based specifications,
                  which can be refined by successively adding
                  constraints. Key concepts of our method are
                  {\em projective views}, {\em separation of
                  proof obligations}, {\em Skolemization} and
                  {\em abstraction}. The method is even
                  applicable to real time systems.",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 ""

  author = 	 "Beimel, Amos and G{\'a}l, Anna and Paterson,
  title = 	 "Lower Bounds for Monotone Span Programs",
  institution =  brics,
  year = 	 1994,
  type = 	 rs,
  number = 	 "RS-94-46",
  address = 	 daimi,
  month = 	 dec,
  note = 	 "14~pp. Appears in " # ieeefocs95 # ", pages
  abstract = 	 "The model of span programs is a linear
                  algebraic model of computation. Lower bounds
                  for span programs imply lower bounds for
                  contact schemes, symmetric branching programs
                  and for formula size. Monotone span programs
                  correspond also to linear secret-sharing
                  schemes. We present a new technique for proving
                  lower bounds for monotone span programs. The
                  main result proved here yields quadratic lower
                  bounds for the size of monotone span programs,
                  improving on the largest previously known
                  bounds for explicit functions. The bound is
                  asymptotically tight for the function
                  corresponding to a class of 4-cliques.",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 ""
  author = 	 "Andersen, J{\o}rgen H. and Kristoffersen,
                  K{\aa}re J. and Larsen, Kim G. and Niedermann,
  title = 	 "Automatic Synthesis of Real Time Systems",
  institution =  brics,
  year = 	 1994,
  type = 	 rs,
  number = 	 "RS-94-45",
  address = 	 iesd,
  month = 	 dec,
  note = 	 "17 pp. Appears in " # lncs944 # ", pages
  abstract = 	 "This paper presents a method for automatically
                  constructing real time systems directly from
                  their specifications. The model--construction
                  problem is considered for implicit
                  specifications of the form: \[ (A_1\,{\mid
                  }\,\ldots\,{\mid}\,A_n\,{\mid}\,X) \,\,\mbox
                  {{\sf sat}}\,\, S \] where $S$ is a real time
                  (logical) specification, $A_1\ldots A_n$ are
                  given (regular) timed agents and the problem is
                  to decide whether there exists (and if possible
                  exhibit) a real time agent $X$ which when put
                  in parallel with $A_1\ldots A_n$ will yield a
                  network satisfying $S$. The method presented
                  proceeds in two steps: first, the implicit
                  specification of $X$ is transformed into an
                  equivalent direct specification of $X$; second,
                  a model for this direct specification is
                  constructed (if possible) using a direct model
                  construction algorithm. A prototype
                  implementation of our method has been added to
                  the real time verification tool EPSILON.",
  linkhtmlabs =  "",
  linkps = 	 ""
  author = 	 "Agerholm, Sten",
  title = 	 "A {HOL} Basis for Reasoning about Functional
  institution =  brics,
  year = 	 1994,
  type = 	 rs,
  number = 	 "RS-94-44",
  address = 	 daimi,
  month = 	 dec,
  note = 	 "PhD thesis. viii+224 pp",
  abstract = 	 "Domain theory is the mathematical theory
                  underlying denotational semantics. This thesis
                  presents a formalization of domain theory in
                  the Higher Order Logic (HOL) theorem proving
                  system along with a mechanization of proof
                  functions and other tools to support reasoning
                  about the denotations of functional programs.
                  By providing a fixed point operator for
                  functions on certain domains which have a
                  special undefined (bottom) element, this
                  extension of HOL supports the definition of
                  recursive functions which are not also
                  primitive recursive. Thus, it provides an
                  approach to the long-standing and important
                  problem of defining non-primitive recursive
                  functions in the HOL system.\bibpar
                  Our philosophy is that there must be a direct
                  correspondence between elements of complete
                  partial orders (domains) and elements of HOL
                  types, in order to allow the reuse of higher
                  order logic and proof infrastructure already
                  available in the HOL system. Hence, we are able
                  to mix domain theoretic reasoning with
                  reasoning in the set theoretic HOL world to
                  advantage, exploiting HOL types and tools
                  directly. Moreover, by mixing domain and set
                  theoretic reasoning, we are able to eliminate
                  almost all reasoning about the bottom element
                  of complete partial orders that makes the LCF
                  theorem prover, which supports a first order
                  logic of domain theory, difficult and tedious
                  to use. A thorough comparison with LCF is
                  The advantages of combining the best of the
                  domain and set theoretic worlds in the same
                  system are demonstrated in a larger example,
                  showing the correctness of a unification
                  algorithm. A major part of the proof is
                  conducted in the set theoretic setting of
                  higher order logic, and only at a late stage of
                  the proof domain theory is introduced to give a
                  recursive definition of the algorithm, which is
                  not primitive recursive. Furthermore, a total
                  well-founded recursive unification function can
                  be defined easily in pure HOL by proving that
                  the unification algorithm (defined in domain
                  theory) always terminates; this proof is
                  conducted by a non-trivial well-founded
                  induction. In such applications, where
                  non-primitive recursive HOL functions are
                  defined via domain theory and a proof of
                  termination, domain theory constructs only
                  appear temporarily.",
  linkhtmlabs =  "",
  linkps = 	 ""
  author = 	 "Aceto, Luca and Jeffrey, Alan~S.~A.",
  title = 	 "A Complete Axiomatization of Timed
                  Bisimulation for a Class of Timed Regular
                  Behaviours (Revised Version)",
  institution =  brics,
  year = 	 1994,
  type = 	 rs,
  number = 	 "RS-94-43",
  address = 	 iesd,
  month = 	 dec,
  note = 	 "18 pp. Appears in {\em Theoretical Computer
                  Science} vol.~152(2) pages 251--268, December
  abstract = 	 "One of the most satisfactory results in
                  process theory is Milner's axiomatization of
                  strong bisimulation for regular CCS. This
                  result holds for open terms with finite-state
                  recursion. Wang has shown that timed
                  bisimulation can also be axiomatized, but only
                  for closed terms without recursion. In this
                  paper, we provide an axiomatization for timed
                  bisimulation of open terms with finite-state
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 ""
  author = 	 "Breslauer, Dany and G{\c{a}}sieniec, Leszek",
  title = 	 "Efficient String Matching on Coded Texts",
  institution =  brics,
  year = 	 1994,
  type = 	 rs,
  number = 	 "RS-94-42",
  address = 	 daimi,
  month = 	 dec,
  note = 	 "20 pp. Appears with the title {\em Efficient
                  String Matching on Packed Texts} in " # lncs937
                  # ", pages 27--40 and in {\em RAIRO
                  Informatique Th{\'e}orique et Applications},
                  30(6):521--544, 1996",
  abstract = 	 "The so called ``four Russians technique'' is
                  often used to speed up algorithms by encoding
                  several data items in a single memory cell.
                  Given a sequence of $n$ symbols over a constant
                  size alphabet, one can encode the sequence into
                  $O(n / \lambda)$ memory cells in $O(\log\lambda
                  )$ time using $n / \log\lambda$
                  This paper presents an efficient CRCW-PRAM
                  string-matching algorithm for coded texts that
                  takes $O(\log\log(m/\lambda))$ time making only
                  $O(n / \lambda)$ operations, an improvement by
                  a factor of $\lambda= O(\log n)$ on the number
                  of operations used in previous algorithms.
                  Using this string-matching algorithm one can
                  test if a string is square-free and find all
                  palindromes in a string in $O(\log\log n)$ time
                  using $n / \log\log n$ processors.",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 ""
  author = 	 "Miltersen, Peter Bro and Nisan, Noam and
                  Safra, Shmuel and Wigderson, Avi",
  title = 	 "On Data Structures and Asymmetric
                  Communication Complexity",
  institution =  brics,
  year = 	 1994,
  type = 	 rs,
  number = 	 "RS-94-41",
  address = 	 daimi,
  month = 	 dec,
  note = 	 "17 pp. Appears in " # acmstoc95 # ", pages
                  103--111. Appears also in {\em Journal of
                  Computer and System Sciences}, 57(1):37--49,
  abstract = 	 "In this paper we consider two party
                  communication complexity when the input sizes
                  of the two players differ significantly, the
                  ``asymmetric'' case. Most of previous work on
                  communication complexity only considers the
                  total number of bits sent, but we study
                  tradeoffs between the number of bits the first
                  player sends and the number of bits the second
                  sends. These types of questions are closely
                  related to the complexity of static data
                  structure problems in the cell probe model. We
                  derive two generally applicable methods of
                  proving lower bounds, and obtain several
                  applications. These applications include new
                  lower bounds for data structures in the cell
                  probe model. Of particular interest is our
                  ``round elimination'' lemma, which is
                  interesting also for the usual symmetric
                  communication case. This lemma generalizes and
                  abstracts in a very clean form the ``round
                  reduction'' techniques used in many previous
                  lower bound proofs.",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 ""
  author = 	 "Aceto, Luca and Ing{\'o}lfsd{\'o}ttir, Anna",
  title = 	 "{CPO} Models for {GSOS} Languages --- Part
                  {I}: Compact {GSOS} Languages",
  institution =  brics,
  year = 	 1994,
  type = 	 rs,
  number = 	 "RS-94-40",
  address = 	 iesd,
  month = 	 dec,
  note = 	 "70 pp. An extended abstract of the paper
                  appears in: {\em Proceedings of CAAP~'95}, LNCS
                  915, 1995, pages 439--453. Full version also
                  appears in {\em Information and Computation},
                  129(2):107--141, September 1996.",
  abstract = 	 "In this paper, we present a general way of
                  giving denotational semantics to a class of
                  languages equipped with an operational
                  semantics that fits the GSOS format of Bloom,
                  Istrail and Meyer. The canonical model used for
                  this purpose will be Abramsky's domain of
                  synchronization trees, and the denotational
                  semantics automatically generated by our
                  methods will be guaranteed to be fully abstract
                  with respect to the finitely observable part of
                  the bisimulation preorder. In the process of
                  establishing the full abstraction result, we
                  also obtain several general results on the
                  bisimulation preorder (including a complete
                  axiomatization for it), and give a novel
                  operational interpretation of GSOS languages",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 ""
  author = 	 "Damg{\aa}rd, Ivan B. and Goldreich, Oded and
                  Wigderson, Avi",
  title = 	 "Hashing Functions can Simplify Zero-Knowledge
                  Protocol Design (too)",
  institution =  brics,
  year = 	 1994,
  type = 	 rs,
  number = 	 "RS-94-39",
  address = 	 daimi,
  month = 	 nov,
  note = 	 "18 pp",
  abstract = 	 "In {\em Crypto93}, Damg{\aa}rd showed that
                  any constant-round protocol in which the
                  verifier sends only independent, random bits
                  and which is zero-knowledge against the {\em
                  honest} verifier can be transformed into a
                  protocol (for the same problem) that is
                  zero-knowledge {\em in general}. His
                  transformation was based on the interactive
                  hashing technique of Naor, Ostrovsky,
                  Venkatesan and Yung, and thus the resulting
                  protocol had very large
                  We adopt Damg{\aa}rd's methods, using ordinary
                  hashing functions, instead of the
                  abovementioned interactive hashing technique.
                  Typically, the protocols we derive have much
                  lower round-complexity than those derived by
                  Damg{\aa}rd's transformation. As in
                  Damg{\aa}rd's transformation, our
                  transformation preserves statistical/perfect
                  zero-knowledge and does not rely on any
                  computational assumptions. However, unlike
                  Damg{\aa}rd's transformation, the new
                  transformation is not applicable to argument
                  systems or to proofs of knowledge",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 ""

  author = 	 "Damg{\aa}rd, Ivan B. and Knudsen, Lars
  title = 	 "Enhancing the Strength of Conventional
  institution =  brics,
  year = 	 1994,
  type = 	 rs,
  number = 	 "RS-94-38",
  address = 	 daimi,
  month = 	 nov,
  note = 	 "12 pp",
  abstract = 	 "We look at various ways of enhancing the
                  strength of conventional cryptosystems such as
                  DES by building a new system which has longer
                  keys and which uses the original system as a
                  building block. We propose a new variant of
                  two-key triple encryption which is not
                  vulnerable to the meet in the middle attack by
                  van Oorschot and Wiener. Under an appropriate
                  assumption on the security of DES, we can prove
                  that our system is at least as hard to break as
                  single DES",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 ""

  author = 	 "van Oosten, Jaap",
  title = 	 "Fibrations and Calculi of Fractions",
  institution =  brics,
  year = 	 1994,
  type = 	 rs,
  number = 	 "RS-94-37",
  address = 	 daimi,
  month = 	 nov,
  note = 	 "21 pp. Appears in {\em Journal of Pure and
                  Applied}, 146(1):77--102, 2000",
  abstract = 	 "Given a fibration ${\cal E}\rightarrow\cal B$
                  and a class $\Sigma$ of arrows of $\cal B$, one
                  can construct the free fibration (on $\cal E$
                  over $\cal B$ such that all reindexing functors
                  over elements of $\Sigma$ are
                  In this work I give an explicit construction of
                  this, and study its properties. For example,
                  the construction preserves the property of
                  being fibrewise discrete, and it commutes up to
                  equivalence with fibrewise exact completions. I
                  show that mathematically interesting situations
                  are examples of this construction. In
                  particular, subtoposes of the effective topos
                  are treated.",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 ""
  author = 	 "Razborov, Alexander A.",
  title = 	 "On provably disjoint {{\bf NP}}-pairs",
  institution =  brics,
  year = 	 1994,
  type = 	 rs,
  number = 	 "RS-94-36",
  address = 	 daimi,
  month = 	 nov,
  note = 	 "27 pp",
  abstract = 	 "In this paper we study the pairs $(U,V)$ of
                  disjoint {\bf NP}-sets representable in a
                  theory $T$ of Bounded Arithmetic in the sense
                  that $T$ proves $U \cap V = \emptyset$. For a
                  large variety of theories $T$ we exhibit a
                  natural disjoint {\bf NP}-pair which is
                  complete for the class of disjoint {\bf
                  NP}-pairs representable in $T$. This allows us
                  to clarify the approach to showing independence
                  of central open questions in Boolean complexity
                  from theories of Bounded Arithmetic initiated
                  in [1]. Namely, in order to prove the
                  independence result from a theory $T$, it is
                  sufficient to separate the corresponding
                  complete {\bf NP}-pair by a (quasi)poly-time
                  computable set. We remark that such a
                  separation is obvious for the theory ${\cal
                  S}(S_2) + {\cal S}\Sigma^b_2 - PIND$ considered
                  in [1], and this gives an alternative proof of
                  the main result from that paper.\bibpar
                  [1] A. Razborov. Unprovability of lower bounds
                  on circuit size in certain fragments of Bounded
                  Arithmetic. To appear in {\em Izvestiya of the
                  RAN}, 1994. ",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 ""
  author = 	 "Brodal, Gerth St{\o}lting",
  title = 	 "Partially Persistent Data Structures of
                  Bounded Degree with Constant Update Time",
  institution =  brics,
  year = 	 1994,
  type = 	 rs,
  number = 	 "RS-94-35",
  address = 	 daimi,
  month = 	 nov,
  note = 	 "24~pp. Appears in {\em Nordic Journal of
                  Computing}, 3(3):238--255, 1996",
  abstract = 	 "The problem of making bounded in-degree and
                  out-degree data structures partially persistent
                  is considered. The node copying method of
                  Driscoll {\it et al.\/} is extended so that
                  updates can be performed in {\em worst-case\/}
                  constant time on the pointer machine model.
                  Previously it was only known to be possible in
                  amortised constant time [Driscoll89].
                  The result is presented in terms of a new
                  strategy for Dietz and Raman's dynamic two
                  player pebble game on graphs.
                  It is shown how to implement the strategy and
                  the upper bound on the required number of
                  pebbles is improved from $2b+2d+O(\sqrt{b})$ to
                  $d+2b$, where $b$ is the bound of the in-degree
                  and $d$ the bound of the out-degree. We also
                  give a lower bound that shows that the number
                  of pebbles depends on the out-degree $d$.",
  linkhtmlabs =  "",
  linkps = 	 ""
  author = 	 "Andersen, Henrik Reif and Stirling, Colin and
                  Winskel, Glynn",
  title = 	 "A Compositional Proof System for the Modal
  institution =  brics,
  year = 	 1994,
  type = 	 rs,
  number = 	 "RS-94-34",
  address = 	 daimi,
  month = 	 oct,
  note = 	 "18~pp. Appears in " # lics9 # ", pages
                  144--153. Superseeded by BRICS Report
  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 = 	 ""
  author = 	 "Sassone, Vladimiro",
  title = 	 "Strong Concatenable Processes: An Approach to
                  the Category of Petri Net Computations",
  institution =  brics,
  year = 	 1994,
  type = 	 rs,
  number = 	 "RS-94-33",
  address = 	 daimi,
  month = 	 oct,
  note = 	 "40 pp. Workshop version appears in " # nwpt6 #
                  ", pages 385--399 with the title {\em An
                  Approach to the Category of Net Computations}.
                  Revised version appears in " # lncs915 # ",
                  pages 334--348 with the title {\em On the
                  Category of {P}etri Net Computations}",
  abstract = 	 "We introduce the notion of {\it strong
                  concatenable process\/} for Petri nets as the
                  least refinement of non-sequential
                  (concatenable) processes which can be expressed
                  abstractly by means of a {\it functor\/} ${\cal
                  Q}[\_]$ from the category of Petri nets to an
                  appropriate category of symmetric strict
                  monoidal categories with free non-commutative
                  monoids of objects, in the precise sense that,
                  for each net~$N$, the strong concatenable
                  processes of~$N$ are isomorphic to the arrows
                  of~${\cal Q}[N]$. This yields an axiomatization
                  of the causal behaviour of Petri nets in terms
                  of symmetric strict monoidal categories.\bibpar
                  In addition, we identify a {\it coreflection\/}
                  right adjoint to ${\cal Q}[\_]$ and we
                  characterize its replete image in the category
                  of symmetric monoidal categories, thus yielding
                  an abstract description of the category of net
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 ""
  author = 	 "Aiken, Alexander and Kozen, Dexter and
                  Wimmers, Ed",
  title = 	 "Decidability of Systems of Set Constraints
                  with Negative Constraints",
  institution =  brics,
  year = 	 1994,
  type = 	 rs,
  number = 	 "RS-94-32",
  address = 	 daimi,
  month = 	 oct,
  note = 	 "33 pp. Appears in {\em Information and Computation},
		  122(1):30-44, October 1995",
  abstract = 	 "Set constraints are relations between sets of
                  terms. They have been used extensively in
                  various applications in program analysis and
                  type inference. Recently, several algorithms
                  for solving general systems of positive set
                  constraints have appeared. In this paper we
                  consider systems of mixed positive and negative
                  constraints, which are considerably more
                  expressive than positive constraints alone. We
                  show that it is decidable whether a given such
                  system has a solution. The proof involves a
                  reduction to a number-theoretic decision
                  problem that may be of independent interest.",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 ""

  author = 	 "Nisan, Noam and Ta-Shma, Amnon",
  title = 	 "Symmetric Logspace is Closed Under
  institution =  brics,
  year = 	 1994,
  type = 	 rs,
  number = 	 "RS-94-31",
  address = 	 daimi,
  month = 	 sep,
  note = 	 "8 pp",
  abstract = 	 "We present a Logspace, many-one reduction
                  from the undirected st-connectivity problem to
                  its complement. This shows that $SL = co -
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 ""

  author = 	 "Husfeldt, Thore",
  title = 	 "Fully Dynamic Transitive Closure in Plane Dags
                  with one Source and one Sink",
  institution =  brics,
  year = 	 1994,
  type = 	 rs,
  number = 	 "RS-94-30",
  address = 	 daimi,
  month = 	 sep,
  note = 	 "26 pp. Appears in " # lncs979 # ", pages
  abstract = 	 "We give an algorithm for the Dynamic
                  Transitive Closure Problem for planar directed
                  acyclic graphs with one source and one sink.
                  The graph can be updated in logarithmic time
                  under arbitrary edge insertions and deletions
                  that preserve the embedding. Queries of the
                  form `is there a directed path from $u$ to
                  $v$?' for arbitrary vertices $u$ and $v$ can be
                  answered in logarithmic time. The size of the
                  data structure and the initialisation time are
                  linear in the number of edges.\bibpar
                  The result enlarges the class of graphs for
                  which a logarithmic (or even polylogarithmic)
                  time dynamic transitive closure algorithm
                  exists. Previously, the only algorithms within
                  the stated resource bounds put restrictions on
                  the topology of the graph or on the delete
                  operation. To obtain our result, we use a new
                  characterisation of the transitive closure in
                  plane graphs with one source and one sink and
                  introduce new techniques to exploit this
                  We also give a lower bound of $\Omega(\log
                  n/\log\log n)$ on the amortised complexity of
                  the problem in the cell probe model with
                  logarithmic word size. This is the first
                  dynamic directed graph problem with almost
                  matching lower and upper bounds.",
  linkhtmlabs =  "",
  linkps = 	 ""
  author = 	 "Cramer, Ronald and Damg{\aa}rd, Ivan B.",
  title = 	 "Secure Signature Schemes Based on Interactive
  institution =  brics,
  year = 	 1994,
  type = 	 rs,
  number = 	 "RS-94-29",
  address = 	 daimi,
  month = 	 sep,
  note = 	 "24~pp. Appears in " # lncs963 # ", pages
  abstract = 	 "A method is proposed for constructing from
                  interactive protocols digital signature schemes
                  secure against adaptively chosen message
                  attacks. Our main result is that practical
                  secure signature schemes can now also be based
                  on computationally difficult problems other
                  than factoring, such as the discrete logarithm
                  More precisely, given only an interactive
                  protocol of a certain type as a primitive, we
                  can build a (non-interactive) signature scheme
                  that is secure in the strongest sense of
                  Goldwasser, Micali and Rivest (GMR): not
                  existentially forgeable under adaptively chosen
                  message attacks. There are numerous examples of
                  primitives that satisfy our conditions, e.g.
                  Feige-Fiat-Shamir, Schnorr, Guillou-Quisquater,
                  Okamoto and Brickell-Mc.Curley.\bibpar
                  In fact, the existence of one-way group
                  homomorphisms is a sufficient assumption to
                  support our construction. As we also
                  demonstrate that our construction can be based
                  on claw-free pairs of trapdoor one-way
                  permutations, our results can be viewed as a
                  generalization of the GMR signature scheme",
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 ""
  author = 	 "Goldreich, Oded",
  title = 	 "Probabilistic Proof Systems",
  institution =  brics,
  year = 	 1994,
  type = 	 rs,
  number = 	 "RS-94-28",
  address = 	 "Department of Applied Mathematics and Computer
                  Science, Weizmann Institute of Science,
                  Rehovot, Israel",
  month = 	 sep,
  note = 	 "19 pp",
  abstract = 	 "Various types of {\em probabilistic} proof
                  systems have played a central role in the
                  development of computer science in the last
                  decade. In this exposition, we concentrate on
                  three such proof systems --- {\em interactive
                  proofs}, {\em zero-knowledge proofs}, and {\em
                  probabilistic checkable proofs} --- stressing
                  the essential role of randomness in each of
                  This exposition is an expanded version of a
                  survey written for the proceedings of the
                  International Congress of Mathematicians ({\em
                  ICM94}) held in Zurich in 1994. It is hope that
                  this exposition may be accessible to a broad
                  audience of computer scientists and
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 ""

  author = 	 "Bra{\"u}ner, Torben",
  title = 	 "A Model of Intuitionistic Affine Logic from
                  Stable Domain Theory (Revised and Expanded
  institution =  brics,
  year = 	 1994,
  type = 	 rs,
  number = 	 "RS-94-27",
  address = 	 daimi,
  month = 	 sep,
  note = 	 "19 pp. Full version of paper appearing in " #
                  lncs820 # ", pages 340--351. This report is a
                  revised and expanded version of DAIMI IR-118",
  abstract = 	 "Girard worked with the category of coherence
                  spaces and continuous stable maps and observed
                  that the functor that forgets the linearity of
                  linear stable maps has a left adjoint. This
                  fundamental observation gave rise to the
                  discovery of Linear Logic. Since then, the
                  category of coherence spaces and linear stable
                  maps, with the comonad induced by the
                  adjunction, has been considered a canonical
                  model of Linear Logic. Now, the same phenomenon
                  is present if we consider the category of pre
                  dI domains and continuous stable maps, and the
                  category of dI domains and linear stable maps;
                  the functor that forgets the linearity has a
                  left adjoint. This gives an alternative model
                  of Intuitionistic Linear Logic. It turns out
                  that this adjunction can be factored in two
                  adjunctions yielding a model of Intuitionistic
                  Affine Logic; the category of pre dI domains
                  and affine stable functions. It is the goal of
                  this paper to show that this category is
                  actually a model of Intuitionistic Affine
                  Logic, and to show that this category moreover
                  has properties which make it possible to use it
                  to model convergence/divergence behaviour and
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 ""
  author = 	 "Riis, S{\o}ren",
  title = 	 "Count($q$) versus the Pigeon-Hole Principle",
  institution =  brics,
  year = 	 1994,
  type = 	 rs,
  number = 	 "RS-94-26",
  address = 	 daimi,
  month = 	 aug,
  note = 	 "3 pp. Appears in {\em Archive for Mathematical
                  Logic\/} 36(3):157--188 (1997) (expanded to a
                  selfcontained paper)",
  abstract = 	 "For each $p \leq 2$ there exist a model
                  ${M\!\!I}^{*}$ of $I\Delta_{0}(\alpha)$ which
                  satisfies the Count($p$) principle. Furthermore
                  if $p$ contain all prime factors of $q$ there
                  exist $n,r \in{M\!\!I}^{*}$ and a bijective map
                  $f \in{\rm Set}({M\!\!I}^{*})$ mapping
                  $\{1,2,...,n\}$ onto $\{1,2,...,n+q^{r}\}$.
                  A corollary is a complete classification of the
                  Count($q$) versus Count($p$) problem. Another
                  corollary solves an open question by M.
  linkhtmlabs =  "",
  linkdvi = 	 "",
  linkps = 	 ""
  author = 	 "Riis, S{\o}ren",
  title = 	 "Bootstrapping the Primitive Recursive
                  Functions by 47 Colors",
  institution =  brics,
  year = 	 1994,
  type = 	 rs,
  number = 	 "RS-94-25",
  address = 	 daimi,
  month = 	 aug,
  note = 	 "5 pp. Improved version appears in {\em Decrete
                  Mathematics} 169(1--3):269--272 (1997) under
                  the title {\em Bootstrapping the Primitive
                  Recursive Functions by Only 27 Colors}",
  abstract = 	 "I construct a concrete coloring of the 3
                  element subsets of $I\!N$. It has the property
                  that each homogeneous set
                  $\{s_{1},s_{2},...,s_{u}\}, u \geq s_{1}$ has
                  its elements spread so much apart that