@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"} @proceedings{BRICS-NS-98-8, title = "Proceedings of the 1998 {APPSEM} Workshop on Normalization by Evaluation, {NBE~'98} Proceedings, {\em(Gothenburg, Sweden, May 8--9, 1998)}", year = 1998, editor = "Danvy, Olivier and Dybjer, Peter", number = "NS-98-8", series = ns, address = daimi, month = dec, organization = brics } @techreport{BRICS-NS-98-7, author = "Power, John", title = "2-Categories", institution = brics, year = 1998, type = ns, number = "NS-98-7", address = daimi, month = aug, note = "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.\bibpar {\bf Contents} \begin{itemize} \item[1] Why 2-categories? \item[2] Calculus in a 2-category \item[3] The calculus of 2-categories \item[4] Coherence \end{itemize} ", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @proceedings{BRICS-NS-98-6, title = "Abstracts of the Workshop on Proof Theory and Complexity, {PTAC~'98}, {\em(Aarhus, Denmark, August 3--7, 1998)}", year = 1998, editor = "Butz, Carsten and Kohlenbach, Ulrich and Riis, S{\o}ren and Winskel, Glynn", number = "NS-98-6", series = ns, address = daimi, month = jul, organization = brics, note = "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). \bibpar The topic of the workshop will be on proof-theory with connections to issues of complexity in the widest sense including e.g.: \begin{enumerate} \item Strength (proof-theoretic and mathematical) of subsystems of second-order arithmetic and type theories. \item Type-free applicative systems (explicit mathematics). \item Complexity of Proof Transformations (cut-elimination, normalization, epsilon-substitution etc.). \item Proofs as Programs. \item Proof Interpretations and their complexity: Realizability and functional interpretations, game theoretic and categorical interpretations. \item Bounded arithmetic and connections to complexity theory (including feasible arithmetic and analysis). \item Proof Complexity of propositional proof systems: resolution, Frege systems, Nullstellensatz proofs etc. \item Interactive and probabilistic proofs. \end{enumerate} 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)", linkhtmlabs = "", linkdvi = "", linkps = "", linkpdf = "" } @proceedings{BRICS-NS-98-5, title = "Proceedings of the Workshop on Semantics of Objects as Processes, {SOAP~'98}, {\em(Aalborg, Denmark, July 18, 1998)}", year = 1998, editor = "H{\"u}ttel, Hans and Nestmann, Uwe", number = "NS-98-5", series = ns, address = iesd, month = jun, organization = brics, note = "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.\bibpar 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.\bibpar 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.\bibpar 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.\bibpar Among the submitted abstracts, six were recommended by the programme committee (Mart{\'\i}n Abadi, Hans H{\"u}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.\bibpar 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", linkhtmlabs = "", linkps = "", linkpdf = "" } @proceedings{BRICS-NS-98-4, title = "Proceedings of the International Workshop on Software Tools for Technology Transfer, {STTT~'98}, {\em(Aalborg, Denmark, July 12--13, 1998)}", year = 1998, editor = "Margaria, Tiziana and Steffen, Bernhard", number = "NS-98-4", series = ns, address = daimi, month = jun, organization = brics, note = "86~pp", abstract = "This volume contains the proceedings of the International Workshop on {\em 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}$ {\em International Colloquium on Automata, Languages, and Programming}.\bibpar 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.\bibpar 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 \begin{itemize} \item a {\bf one-day Workshop}, on {\em July 12th}, whose eight talks were organized in three sessions: \begin{itemize} \item {\em Verification of Code Generation}: compiler-specific and program-specific verification. \item {\em Model Checking}: variants, also comprising real time aspects. \item {\em Technology Transfer}: initiatives and projects. \end{itemize} \item a {\bf two-days Tool Exhibition}, on {\em 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. \end{itemize} ", linkhtmlabs = "", linkps = "", linkpdf = "" } @techreport{BRICS-NS-98-3, author = "Klarlund, Nils and M{\o}ller, Anders", title = "{\sf MONA} Version 1.2 --- User Manual", institution = brics, year = 1998, type = ns, number = "NS-98-3", address = daimi, month = jun, note = "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 \htmladdnormallink {http://www.brics.dk/mona}{http://www.brics.dk/mona} for further information", linkhtmlabs = "", linkps = "", linkpdf = "" } @proceedings{BRICS-NS-98-2, title = "Proceedings of the Workshop on Applicability of Formal Methods, {AFM~'98}, {\em(Aarhus, Denmark, June 2, 1998)}", year = 1998, editor = "Mosses, Peter D. and Engberg, Uffe H.", number = "NS-98-2", series = ns, address = daimi, month = jun, note = "94~pp" } @proceedings{BRICS-NS-98-1, title = "Preliminary Proceedings of the 1998 APPSEM Workshop on Normalization by Evaluation, {NBE~'98}, {\em(Gothenburg, Sweden, May 8--9, 1998)}", year = 1998, editor = "Danvy, Olivier and Dybjer, Peter", number = "NS-98-1", series = ns, address = daimi, month = may, organization = brics }