This document is also available as
PostScript
and
DVI.
 NS988

Olivier Danvy and Peter Dybjer, editors.
Proceedings of the 1998 APPSEM Workshop on Normalization by
Evaluation, NBE '98 Proceedings, (Gothenburg, Sweden, May 89,
1998), December 1998.
 NS987

PostScript,
PDF,
DVI.
John Power.
2Categories.
August 1998.
18 pp.
Abstract: These notes constitute lecture notes to accompany a
course on categories at BRICS in the Computer Science Department of the
University of Aarhus in March 1998. Each section corresponds to one
lecture.
Contents
 1
 Why 2categories?
 2
 Calculus in a 2category
 3
 The calculus of 2categories
 4
 Coherence
.
 NS986

PostScript,
PDF,
DVI.
Carsten Butz, Ulrich Kohlenbach, Søren
Riis, and Glynn Winskel, editors.
Abstracts of the Workshop on Proof Theory and Complexity,
PTAC '98, (Aarhus, Denmark, August 37, 1998), July 1998.
vi+16 pp.
Abstract: This small booklet contains the titles and abstracts
of the talks given at the workshop Proof Theory and Complexity (PTAC'98),
hosted by BRICS during the first week of August 98 (August 3  August 7).
The topic of the workshop will be on prooftheory with connections to
issues of complexity in the widest sense including e.g.:
 Strength (prooftheoretic and mathematical) of subsystems of
secondorder arithmetic and type theories.
 Typefree applicative
systems (explicit mathematics).
 Complexity of Proof Transformations
(cutelimination, normalization, epsilonsubstitution etc.).
 Proofs as
Programs.
 Proof Interpretations and their complexity: Realizability and
functional interpretations, game theoretic and categorical interpretations.
 Bounded arithmetic and connections to complexity theory (including
feasible arithmetic and analysis).
 Proof Complexity of propositional
proof systems: resolution, Frege systems, Nullstellensatz proofs etc.
 Interactive and probabilistic proofs.
There were two
preparatory lectures during the week before the workshop (by E. Palmgren and
V. Orevkovabstracts can be obtained from the BRICS homepage), and there
are two special lectures in connection with the workshop that take place
during this week (by A. Feferman and A. Wigderson).
 NS985

PostScript,
PDF.
Hans Hüttel and Uwe Nestmann, editors.
Proceedings of the Workshop on Semantics of Objects as
Processes, SOAP '98, (Aalborg, Denmark, July 18, 1998), June 1998.
50 pp.
Abstract: One of the most widespread programming paradigms
today is that of objectoriented programming. With the growing popularity of
the language C++ and the advent of Java as the language of choice for the
World Wide Web, objectoriented programs have taken centre stage.
Consequently, the past decade has seen a flurry of interest within the
programming language research community for providing a firm semantic basis
for objectoriented constructs.
Recently, there has been growing
interest in studying the behavioural properties of objectoriented programs
using concepts and ideas from the world of concurrent process calculi, in
particular calculi with some notion of mobility. Not only do such calculi, as
the wellknown calculus by Milner and others, have features like
references and scoping in common with objectoriented languages; they also
provide one with a rich vocabulary of reasoning techniques firmly grounded in
structural operational semantics.
The process calculus view has
therefore proven to be advantageous in many ways for semantics and
verification issues. On the one hand, the use of encodings of objectoriented
languages into existing typed mobile process calculi enables formal reasoning
about the correctness of programs; on the other hand, using standard
techniques from concurrency theory in the setting of calculi for objects may
help in reasoning about objects, e.g. by finding appropriate and
mathematically tractable notions of behavioural equivalences. Encodings may
also help clarify the overlap and differences of objects and processes, and
suggest how to integrate them best in languages with both.
The aim of
the oneday SOAP workshop, which is a satellite workshop of ICALP 98, has
been to bring together researchers working mainly in this area, but in
related fields as well, where other process models or calculi are used as a
basis for the semantics of objects.
Among the submitted abstracts, six
were recommended by the programme committee (Martín Abadi, Hans
Hüttel, Josva Kleist, and Uwe Nestmann) and are presented in these
proceedings. According to the more informal character of the workshop, there
was no formal refereeing process. It is expected that the abstracts presented
in these proceedings will appear elsewhere at other conferences or in
journals.
We would like to thank the organizers of ICALP '98 for
helping us set up the SOAP workshop and BRICS for the publication of these
proceedings.
 NS984

PostScript,
PDF.
Tiziana Margaria and Bernhard Steffen,
editors.
Proceedings of the International Workshop on Software Tools for
Technology Transfer, STTT '98, (Aalborg, Denmark, July 1213, 1998),
June 1998.
86 pp.
Abstract: This volume contains the proceedings of the
International Workshop on Software Tools for Technology Transfer,
STTT'98, which took place in Aalborg (Denmark) on July 1213 1998, as a
satellite of ICALP'98, the 25 International Colloquium on
Automata, Languages, and Programming.
Tool support for the
development of reliable and correct computer systems is in fact of growing
importance: a wealth of design methodologies, algorithms, and associated
tools have been developed in different areas of computer science. However,
each area has its own culture and terminology, preventing researchers from
taking advantage of the results obtained by colleagues in other fields: tool
builders often are unaware of, and thus unable to use, work done by others.
The situation is even more critical when considering the transfer of
technology into industrial practice.
STTT'98 addressed this situation
by providing a forum for discussion of all aspects of tools that aid in the
development of computer systems in the light of a possible tooloriented link
between academic research and industrial practice. Accordingly, the event
comprised
 a oneday Workshop, on July 12th,
whose eight talks were organized in three sessions:
 Verification of Code Generation: compilerspecific and programspecific
verification.
 Model Checking: variants, also comprising real time
aspects.
 Technology Transfer: initiatives and projects.
 a twodays Tool Exhibition, on July 12th and
13rd, which, in addition to the tools presented at the workshop, comprised a
demonstration of the three tools described at the end of the proceedings.
.
 NS983

PostScript,
PDF.
Nils Klarlund and Anders Møller.
MONA Version 1.2  User Manual.
June 1998.
60 pp.
Abstract: This manual describes MONA version 1.2 as released
June 1998. Sections 2 and 3 describe the features of the MONA tool through a
number of examples. Section 4 discusses the automatonlogic connection and
the MONA compilation semantics. In Section 5, the decision procedure for WS2S
is presented along with the MONA concept of a tree automaton. Section 6
discusses our plans for future work. In the appendices, the full syntax is
defined, the commandline usage of MONA is shown, and the MONA BDDpackage is
described. The complete source code for MONA version 1.2 is available for
educational and research purposes. Please visit the MONA home page at
http://www.brics.dk/mona
for
further information.
 NS982

Peter D. Mosses and Uffe H. Engberg, editors.
Proceedings of the Workshop on Applicability of Formal Methods,
AFM '98, (Aarhus, Denmark, June 2, 1998), June 1998.
94 pp.
 NS981

Olivier Danvy and Peter Dybjer, editors.
Preliminary Proceedings of the 1998 APPSEM Workshop on
Normalization by Evaluation, NBE '98, (Gothenburg, Sweden, May 89,
1998), May 1998.
