@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-NS-95-6,
author = "Srinivasan, Aravind",
title = "The Role of Randomness in Computation",
institution = brics,
year = 1995,
type = ns,
number = "NS-95-6",
address = daimi,
month = nov,
note = "iv+99 pp",
abstract = "The course was intended to serve both as a
tutorial introduction to the role of randomness
in computation, specifically in algorithms and
complexity, and as a forum for the discussion
of the most recent research in the area. The
course was organised into a sequence of 6
lectures:
\begin{enumerate}
\item Introduction,
\item Randomness in Distributed Computing,
\item Derandomisation,
\item Random Sampling,
\item The Lovasz Local Lemma,
\item Weak Random Sources.
\end{enumerate}
In addition, the course was supplemented by a
talk on ``Improved Approximation Algorithms for
Packing and Covering Problems''.",
linkhtmlabs = ""
}
@techreport{BRICS-NS-95-5,
author = "Paige, Robert",
title = "Analysis and Transformation of Set-Theoretic
Languages. Mini-Course",
institution = brics,
year = 1995,
type = ns,
number = "NS-95-5",
address = "",
month = aug,
note = "iv+157 pp",
abstract = "The course was on how types and
transformations can be used to integrate
algorithm design and analysis, program
development, and high level compilation of set
theoretic programming languages. Topics:
\begin{itemize}
\item Introduction to SETL and sources of
inefficiency; program improvement by finite
differencing,
\item Program improvement by real-time
simulation of a typed set machine (equipped
with high level input/output) on a RAM,
\item Reconstruction and extension of the
linear time fragment of Willard's database
predicate retrieval theory,
\item Design of A linear time fixed point
language; experiments in productivity of
algorithm implementation.
\end{itemize}
",
linkhtmlabs = ""
}
@techreport{BRICS-NS-95-4,
author = "Gurevich, Yuri and B{\"o}rger, Egon",
title = "Evolving Algebras. {M}ini-Course",
institution = brics,
year = 1995,
type = ns,
number = "NS-95-4",
address = "",
month = jul,
note = "iv+222 pp",
abstract = "Professors Egon B{\"o}rger (Univ.\ of Pisa)
and Yuri Gurevich (Univ.\ of Michigan) visited
BRICS during August 1995\@. From 7--10 August
they held an intensive mini-course of 14 double
lectures on Evolving Algebras: their framework
for modelling algorithms and languages, with
links to both Complexity Theory and Semantics.
The background and interests of both lecturers
fitted particularly well with the BRICS idea of
synergy between Algorithms and Complexity
Theory, Semantics, and Logic.\bibpar
The course was attended by 12 PhD students.
Gurevich's lectures on the basic concepts and
definitions of evolving algebras were all
prepared specially for the course, and
supported by a large collection of papers from
the literature. B{\"o}rger's lectures on
applications of evolving algebras were based on
some of his latest papers.\bibpar
The course was organized by Peter D. Mosses.
BRICS is very grateful to the lecturers for
their efforts, during what turned out to be
quite a hot week!",
linkps = ""
}
@techreport{BRICS-NS-95-3,
author = "Gordon, Andrew D.",
title = "Bisimilarity as a Theory of Functional
Programming. {M}ini-Course",
institution = brics,
year = 1995,
type = ns,
number = "NS-95-3",
address = "University of Cambridge Computer Laboratory",
month = jul,
note = "iv+59 pp",
abstract = "Operational intuition is central to computer
science. These notes introduce functional
programmers to operational semantics and
operational equivalence. We show how the idea
of bisimilarity from CCS may be applied to
deterministic functional languages. On
elementary operational grounds it justifies
equational reasoning and proofs about infinite
streams.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@proceedings{BRICS-NS-95-2,
title = "Proceedings of the Workshop on Tools and Algorithms
for The Construction and Analysis of Systems, TACAS
{\em(Aarhus, Denmark, 19--20 May, 1995)}",
year = 1995,
editor = "Engberg, Uffe H. and Larsen, Kim G. and Skou, Arne",
number = "NS-95-2",
series = ns,
address = daimi,
month = may,
organization = brics,
note = "vi+334~pp. Selected papers appears in " # lncs1019,
abstract = "The aim of the workshop on {\em Tools and Algorithms
for the Construction and Analysis of Systems\/},
TACAS, is to bring together researchers and
practitioners interested in the development and
application of tools and algorithms for
specification, verification, analysis and
construction of distributed systems. The overall
goal of the workshop is to compare the various
methods and the degree to which they are supported
by interacting or fully automatic tools.\bibpar The
23 papers of the proceedings cover the following
topics: refinement-based verification and
construction techniques; compositional verification
methodologies; analysis and verification via
theorem-proving; decision procedures for
verification and analysis; specification formalisms,
including process algebras and temporal and modal
logics; analysis techniques for real-time and/or
probabilistic systems; approaches for value-passing
systems, tool sets for verification and analysis
case studies. There were special sessions for
demonstration of verification tools.",
linkhtmlabs = "",
linkpdf = "",
linkps = ""
}
@techreport{BRICS-NS-95-1,
author = "Walukiewicz, Igor",
title = "Notes on the Propositional $\mu$-calculus:
Completeness and Related Results",
institution = brics,
year = 1995,
type = ns,
number = "NS-95-1",
address = daimi,
month = feb,
note = "54 pp",
abstract = "In this notes we consider propositional $\mu
$-calculus as introduced by Kozen. The main
purpose of these notes is to present the
completeness proof of the Kozen's
axiomatisation of the $\mu$-calculus. To
achieve this goal we develop tools which allow
us to give relatively simple proofs of results
for the logic like:
\begin{itemize}
\item syntactic characterisation of
satisfiability and validity,
\item small model theorem,
\item decidability,
\item equivalence of the $\mu$-calculus over
binary trees and Rabin automata,
\item a notion of disjunctive formula and the
proof that every formula is equivalent to a
disjunctive formula,
\item linear satisfiability checking algorithm
for disjunctive formulas.
\end{itemize}
These notes are intended to supplement a 6
hours course given in February 1995 at BRICS
centre.",
linkhtmlabs = "",
linkps = ""
}