BRICS Notes Series, Abstracts, 1998

July 7, 2003

This document is also available as PostScript and DVI.

Bibliography

NS-98-8
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.

NS-98-7
PostScript, PDF, DVI.
John Power.
2-Categories.
August 1998.
18 pp.
Abstract: These notes constitute lecture notes to accompany a course on $2$-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 2-categories?
2
Calculus in a 2-category
3
The calculus of 2-categories
4
Coherence
.

NS-98-6
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 3-7, 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 proof-theory with connections to issues of complexity in the widest sense including e.g.:
  1. Strength (proof-theoretic and mathematical) of subsystems of second-order arithmetic and type theories.
  2. Type-free applicative systems (explicit mathematics).
  3. Complexity of Proof Transformations (cut-elimination, normalization, epsilon-substitution etc.).
  4. Proofs as Programs.
  5. Proof Interpretations and their complexity: Realizability and functional interpretations, game theoretic and categorical interpretations.
  6. Bounded arithmetic and connections to complexity theory (including feasible arithmetic and analysis).
  7. Proof Complexity of propositional proof systems: resolution, Frege systems, Nullstellensatz proofs etc.
  8. Interactive and probabilistic proofs.
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).

NS-98-5
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 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 $\pi$-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 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.

NS-98-4
PostScript, PDF.
Tiziana Margaria and Bernhard Steffen, editors.
Proceedings of the International Workshop on Software Tools for Technology Transfer, STTT '98, (Aalborg, Denmark, July 12-13, 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 12-13 1998, as a satellite of ICALP'98, the 25$^{th}$ 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 comprised
  • a one-day Workshop, on July 12th, whose eight talks were organized in three sessions:
    • Verification of Code Generation: compiler-specific and program-specific verification.
    • Model Checking: variants, also comprising real time aspects.
    • 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.
.

NS-98-3
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 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 http://www.brics.dk/mona for further information.

NS-98-2
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.

NS-98-1
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.
 
Last modified: 2003-06-07 by webmaster.