This document is also available as
Olivier Danvy and Peter Dybjer, editors.
Proceedings of the 1998 APPSEM Workshop on Normalization by
Evaluation, NBE '98 Proceedings, (Gothenburg, Sweden, May 8-9,
1998), December 1998.
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
- Why 2-categories?
- Calculus in a 2-category
- The calculus of 2-categories
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 3-7, 1998), July 1998.
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 proof-theory with connections to
issues of complexity in the widest sense including e.g.:
There were two
preparatory lectures during the week before the workshop (by E. Palmgren and
V. Orevkov--abstracts 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).
- Strength (proof-theoretic and mathematical) of subsystems of
second-order arithmetic and type theories.
- Type-free applicative
systems (explicit mathematics).
- Complexity of Proof Transformations
(cut-elimination, normalization, epsilon-substitution etc.).
- Proofs as
- 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.
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.
Abstract: One of the most widespread programming paradigms
today is that of object-oriented programming. With the growing popularity of
the language C++ and the advent of Java as the language of choice for the
World Wide Web, object-oriented 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 object-oriented constructs.
Recently, there has been growing
interest in studying the behavioural properties of object-oriented 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 well-known -calculus by Milner and others, have features like
references and scoping in common with object-oriented 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 object-oriented
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 one-day 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
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
Tiziana Margaria and Bernhard Steffen,
Proceedings of the International Workshop on Software Tools for
Technology Transfer, STTT '98, (Aalborg, Denmark, July 12-13, 1998),
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 12-13 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 tool-oriented link
between academic research and industrial practice. Accordingly, the event
- a one-day Workshop, on July 12th,
whose eight talks were organized in three sessions:
- Verification of Code Generation: compiler-specific and program-specific
- Model Checking: variants, also comprising real time
- Technology Transfer: initiatives and projects.
- a two-days 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.
Nils Klarlund and Anders Møller.
MONA Version 1.2 -- User Manual.
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 automaton-logic 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 command-line usage of MONA is shown, and the MONA BDD-package 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
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.
Olivier Danvy and Peter Dybjer, editors.
Preliminary Proceedings of the 1998 APPSEM Workshop on
Normalization by Evaluation, NBE '98, (Gothenburg, Sweden, May 8-9,
1998), May 1998.