@string{brics = "{BRICS}"}
@string{daimi = "Department of Computer Science, University of Aarhus"}
@string{iesd = "Department of Computer Science, Institute
of Electronic Systems, Aalborg University"}
@string{rs = "Research Series"}
@string{ns = "Notes Series"}
@string{ls = "Lecture Series"}
@string{ds = "Dissertation Series"}
@techreport{BRICS-RS-98-55,
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 = ""
}
@techreport{BRICS-RS-98-54,
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
RS-99-27}{http://www.brics.dk/RS/99/27/}",
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
scope.\bibpar
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:
\begin{itemize}
\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.
\end{itemize}
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
time.\bibpar
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 = ""
}
@techreport{BRICS-RS-98-53,
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 = ""
}
@techreport{BRICS-RS-98-52,
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 = ""
}
@techreport{BRICS-RS-98-51,
author = "Jensen, Peter Krogsgaard",
title = "Automated Modeling of Real-Time
Implementation",
institution = brics,
year = 1998,
type = rs,
number = "RS-98-51",
address = iesd,
month = dec,
note = "9~pp. Appears in " # ieeease98ds # ", pages
17--20",
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 = ""
}
@techreport{BRICS-RS-98-50,
author = "Aceto, Luca and Ing{\'o}lfsd{\'o}ttir, Anna",
title = "Testing {Hennessy-Milner} Logic with
Recursion",
institution = brics,
year = 1998,
type = rs,
number = "RS-98-50",
address = iesd,
month = dec,
note = "15~pp. Appears in " # lncs1578 # ", pages
41--55",
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 = ""
}
@techreport{BRICS-RS-98-49,
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
20--34",
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
consideration",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-98-48,
author = "Aceto, Luca and Bouyer, Patricia and
Burgue{\~n}o, Augusto and Larsen, Kim G.",
title = "The Power of Reachability Testing for Timed
Automata",
institution = brics,
year = 1998,
type = rs,
number = "RS-98-48",
address = iesd,
month = dec,
note = "12~pp. Appears in " # lncs1530 # ", pages
245--256",
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 = ""
}
@techreport{BRICS-RS-98-47,
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
341--353",
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
variables.\bibpar
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
runtime.\bibpar
We further report on how the symbolic
state-space exploration itself may be carried
out using CDD's",
linkhtmlabs = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-98-46,
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
differences",
linkhtmlabs = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-98-45,
author = "Jensen, Morten Vadsk{\ae}r and Nielsen,
Brian",
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
377--387",
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
$47:1$.\bibpar
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
effort",
linkhtmlabs = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-98-44,
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
objects.\bibpar
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 = ""
}
@techreport{BRICS-RS-98-43,
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
216--240",
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
tools.\bibpar
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
advantageous",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-98-42,
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 = ""
}
@techreport{BRICS-RS-98-41,
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 = ""
}
@techreport{BRICS-RS-98-40,
author = "Andersen, Henrik Reif and Stirling, Colin and
Winskel, Glynn",
title = "A Compositional Proof System for the Modal
$\mu$-Calculus",
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 = ""
}
@techreport{BRICS-RS-98-39,
author = "Fridlender, Daniel",
title = "An Interpretation of the {F}an Theorem in Type
Theory",
institution = brics,
year = 1998,
type = rs,
number = "RS-98-39",
address = daimi,
month = dec,
note = "15~pp. Appears in " # lncs1657 # ", pages
93--105",
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 = ""
}
@techreport{BRICS-RS-98-38,
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 = ""
}
@techreport{BRICS-RS-98-37,
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
56--73",
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
adversaries.\bibpar
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
intervals",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-98-36,
author = "Cramer, Ronald and Damg{\aa}rd, Ivan B. and
Dziembowski, Stefan and Hirt, Martin and Rabin,
Tal",
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
311--326",
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 = ""
}
@techreport{BRICS-RS-98-35,
author = "Danvy, Olivier and Yang, Zhe",
title = "An Operational Investigation of the {CPS}
Hierarchy",
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
hierarchy.\bibpar
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 = ""
}
@techreport{BRICS-RS-98-34,
author = "Binderup, Peter G. and Frandsen, Gudmund
Skovbjerg and Miltersen, Peter Bro and Skyum,
Sven",
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},
38:17--29",
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 = ""
}
@techreport{BRICS-RS-98-33,
author = "H{\"u}ttel, Hans and Kleist, Josva and
Nestmann, Uwe and Merro, Massimo",
title = "Migration = Cloning ; Aliasing (Preliminary
Version)",
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 = ""
}
@techreport{BRICS-RS-98-32,
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
331--345",
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
problem",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-98-31,
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
42--58",
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
work",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-98-30,
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
property.\bibpar
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 = ""
}
@techreport{BRICS-RS-98-29,
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
106--121",
abstract = "
This paper presents the first efficient
statistical zero-knowledge protocols to prove
statements such as:
\begin{itemize}
\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.
\end{itemize}
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
known.\bibpar
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 = ""
}
@techreport{BRICS-RS-98-28,
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 = ""
}
@techreport{BRICS-RS-98-27,
author = "Camenisch, Jan and Michels, Markus",
title = "A Group Signature Scheme Based on an
{RSA}-Variant",
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 = ""
}
@techreport{BRICS-RS-98-26,
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
congruent",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = ""
}
@techreport{BRICS-RS-98-25,
author = "Dubhashi, Devdatt P.",
title = "{T}alagrand's Inequality in Hereditary
Settings",
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 = ""
}
@techreport{BRICS-RS-98-24,
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
60--70",
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 = ""
}
@techreport{BRICS-RS-98-23,
author = "Dubhashi, Devdatt P.",
title = "Martingales and Locality in Distributed
Computing",
institution = brics,
year = 1998,
type = rs,
number = "RS-98-23",
address = daimi,
month = oct,
note = "19~pp. Appears in " # lncs1530 # ", pages
174--185",
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 = ""
}
@techreport{BRICS-RS-98-22,
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
581--596",
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 = ""
}
@techreport{BRICS-RS-98-21,
author = "Power, John and Cattani, Gian Luca and
Winskel, Glynn",
title = "A Representation Result for Free
Cocompletions",
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 = ""
}
@techreport{BRICS-RS-98-20,
author = "Riis, S{\o}ren and Sitharam, Meera",
title = "Uniformly Generated Submodules of Permutation
Modules",
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)