Preface: Volume 23, Issue 1

This volume contains the Proceedings of A Tutorial Workshop on Realizability Semantics and Applications. The workshop was associated to the 1999 Federated Logic Conference, held in Trento, Italy, from June 30 to July 1, 1999.There has been recently a reawaking of interest in many aspects of realizability interpretations---especially as regards semantics of type theories for constructive reasoning and semantics of programming languages. As the details of realizability can be quite technical, it seemed appropriate to have a tutorial workshop, connected to the Federated Logic Conference, aimed at offering presentations of the various aspects of realizability and directed to a wide audience, not necessarily only for the experts in the field.The Tutorial Workshop on Realizability Semantics and Applications was proposed to the 1999 Federated Logic Conference, Trento, June 29-July 12, 1999, was accepted, and is organized around several tutorial lectures on history, basic definitions and results, recent applications, connections to category theory and then offers a few contributed research talks of 30 minutes each.The Tutorial Presenters are:

Full-size image

     

Preface: Volume 39, Issue 2

ForewordThe main mathematical disciplines that have been used in theoretical computer science are discrete mathematics (especially, graph theory and ordered structures), logics (mostly proof theory for all kinds of logics, classical, intuitionistic, modal etc.) and category theory (cartesian closed categories, topoi etc.). General Topology has also been used for instance in denotational semantics, with relations to ordered structures in particular.Recently, ideas and notions from mainstream “geometric” topology and algebraic topology have entered the scene in Concurrency Theory and Distributed Systems Theory (some of them based on older ideas). They have been applied in particular to problems dealing with coordination of multi-processor and distributed systems. Among those are techniques borrowed from algebraic and geometric topology: Simplicial techniques have led to new theoretical bounds for coordination problems. Higher dimensional automata have been modelled as cubical complexes with a partial order reflecting the time flows, and their homotopy properties allow to reason about a system's global behaviour.This workshop aims at bringing together researchers from both the mathematical (geometry, topology, algebraic topology etc.) and computer scientific side (concurrency theorists, semanticians, researchers in distributed systems etc.) with an active interest in these or related developments.It follows the first workshop on the subject “Geometric and Topological Methods in Concurrency Theory” which has been held in Aalborg, Denmark, in June 1999.The Workshop has been financially supported by Hewlett Packard's Basic Research Institute in the Mathematical Sciences (Bristol, England), the Commissariata l'Energie Atomique (CEA Saclay, France) and the Basic Research Institute in Computer Science (Aarhus, Denmark); I do thank these institutions for this, and more specifically Jeremy Gunawardena and Uffe Engberg. I also wish to thank the referees, the authors and the programme committee members for their very precise and timely job. Many thanks are also due to Michael Mislove who kindly supported the workshop by letting us submit the papers through the Electronic Notes in Theoretical Computer Science. Last but not least, I wish to thank the Concur organizers, Catuscia Palamidessi and Dale Miller, and the Workshop coordinator, Uwe Nestmann, for making this possible.     

Preface: Volume 68, Issue 2

The EXPRESS workshops aim at bringing together researchers interested in the relations between various formal systems, particularly in the field of Concurrency. More specifically, they focus on the comparison between programming concepts (such as concurrent, functional, imperative, logic and object-oriented programming) and between mathematical models of computation (such as process algebras, Petri nets, event structures, modal logics, rewrite systems etc.) on the basis of their relative expressive power.For online-information see http://express02.epfl.ch/.The EXPRESS workshops were originally held as meetings of the HCM project EXPRESS, which was active with the same focus from January 1994 till December 1997. The first three workshops were held respectively in Amsterdam (1994, chaired by Frits Vaandrager), Tarquinia (1995, chaired by Rocco De Nicola), and Dagstuhl (1996, co-chaired by Ursula Goltz and Rocco De Nicola). The workshop in 1997, which took place in Santa Margherita Ligure and was co-chaired by Catuscia Palamidessi and Joachim Parrow, was organized as a conference with a call for papers and a significant attendance from outside the project. The 1998 workshop was held as a satellite workshop of the CONCUR'98 conference in Nice, co-chaired by Ilaria Castellani and Catuscia Palamidessi, and like on that occasion EXPRESS'99 was hosted by the CONCUR'99 conference in Eindhoven, co-chaired by Ilaria Castellani and Björn Victor. The EXPRESS'00 workshop was held as a satellite workshop of CONCUR 2000, Pennsylvania State University, USA, co-chaired by Luca Aceto and Björn Victor. The EXPRESS'01 workshop was held at BRICS, Aalborg University as a satellite of CONCUR'01 and was co-chaired by Luca Aceto and Prakash Panangaden.In addition to the nine accepted (out of 30 submitted) papers presented at the workshop, this collection also contains the abstracts of the two invited talks by Catuscia Palamidessi and Igor Walukiewicz. We would like to thank the authors of the submitted papers, the invited speakers, and the members of the program committee for their contribution to both the meeting and this volume. We also would like to thank EPFL for the printing and Michael Mislove and Simon Kramer for his help with the editing of the preliminary proceedings, the CONCUR organizing committee at Brno University for hosting EXPRESS'02, especially the workshop coordinator Antonín Kucera for further local organization.EXPRESS'02 Programme CommitteeMartin Berger (U. London, UK), Alan Jeffrey (DePaul U., USA), Barbara König (TU München, DE), Francois Laroussinie (ENS Cachan, FR), James Leifer (INRIA Rocquencourt, FR), Massimo Merro (EPFL, CH), Faron Moller (U. Wales, Swansea, UK), Uwe Nestmann (EPFL, CH), Prakash Panangaden (McGill U., CA), Arend Rensink (U. Twente, NL), Peter Sewell (U. Cambridge, UK), Gianluigi Zavattaro (U. Bologna, IT),EXPRESS'02 Additional RefereesLuca Aceto, Alessandro Aldini, Paolo Baldan, Paolo Ballarini, Béatrice Bérard, Henrik Bohnenkamp, Alexandre Boisseau, Mario Bravetti, Roberto Bruni, Marzia Buscemi, Nadia Busi, Didier Caucal, Vincent Cremet, Silvano Dal-Zilio, Vincent Danos, Stéphane Demri, Simon Gay, Daniel Hirschkoff, Michael Huth, Ole Høgh Jensen, Astrid Kiehn, Huimin Lin, Sergio Maffeis, Monika Maidl, Nicolas Markey, Fabio Martinelli, Robin Milner, Francesco Zappa Nardelli, Mikkel Nygaard, Martin Otto, Laure Petrucci, Carla Piazza, Jorge Sousa Pinto, Rosario Pugliese, Marina Ribaudo, Christine Röckl, Stefan Römer, Alan Schmitt, Philippe Schnoebelen, Stefan Schwoon, Martin Steffen, Simone Tini, Björn Victor, Walter Vogler, Heike Wehrheim, Lucian Wischik, Pascal Zimmer.     

Preface: Volume 65, Issue 2

Semantics preservation between source and target program is the commonly accepted minimum requirement to be ensured by compilers. It is the key term compiler verification and optimization are centered around. The precise meaning, however, is often only implicit, e.g.~when tacitly exploiting the scope provided by often in part loose specifications of the semantics of the considered languages. As a rule of thumb, verification tends to interpret semantics preservation in a very tight sense, not only but also to simplify the verification task. Optimization generally prefers a more liberal view in order to enable more powerful transformations otherwise excluded. In each case the semantics of the underlying languages and the preservation of the semantics of the considered programs are the surveyor's rod of admissibility. While undisputed on the level of these abstract terms, the adequate perception of preservation is still an issue of scientific research, which, e.g., depends and varies fluently with the application context (compiling and optimizing “stand-alone” applications, communicating systems, reactive systems, etc.).The aim of the workshop is to bring together researchers and practitioners working on optimizing and verifying compilation as well as on related fields such as programming language design and semantics in order to plumb the mutual impact of these fields on each other, the degrees of freedom optimizers and verifiers have, to bridge the gap between the communities, and to stimulate synergies.The contributed papers accepted for presentation at the workshop and an invited presentation by Gerhard Goos discuss topics such as certifying compilation, verifying compilation, translation validation, and optimization showing both the breadth of research in the fields of optimizing and verifying compilation and their interdependencies as well as the diversity of approaches for addressing and handling them. In the invited keynote speech, Gerhard Goos emphasizes that it is not the compiler but the code generated by it which must be correct. He points out that this subtle difference provides the key for reusing standard compiler architecture, tools and methods in a verifying compiler. In the first contributed paper, Lenore Zuck et al. demonstrate how the correctness of optimizing loop transformations can be checked without proving the correctness of the compiler itself. This technique is called translation validation. Glesner et al. show how to construct correct code-generators for embedded systems. They use a similar technology as Zuck et al. Frederiksen subsequently discusses correctness proofs of global optimizations. These optimizations are modeled as conditional graph-rewrite rules. Nguyen and Irigoin discuss in their paper how to verify aliases in FORTRAN. The non-presence of aliases is an important pre-condition of many optimizations. Shashidar et al. also discuss correctness of loop transformations. In contrast to the approach of Zuck et al.~they distinguish the correctness proof for transformations and their implementation. Jamarillo et al. use translation validation for checking the correctness of some transformations at lower levels of compilers such as register allocation. Goerigk, finally, discusses notions of compiler correctness and shows how they apply to optimizations.The papers in this volume were reviewed by the members of the program committee consisting, besides the editors, of

• Rajiv Gupta, University of Arizona, Tucson, AZ, USA, gupta@cs.arizona.edu

• James R. Larus, Microsoft Research, Redmond, WA, USA, larus@microsoft.com

• Robert Morgan, Compaq Computer Corporation, Nashua, NH, USA, bob.morgan@compaq.com

• J Strother Moore, University of Texas at Austin, TX, USA, Moore@cs.utexas.edu

• Markus Müller-Olm, Universität Dortmund, Germany, mmo@ls5.cs.uni-dortmund.de

• George C. Necula, University of California at Berkely, CA, USA, necula@cs.berkeley.edu

• John Whaley, IBM Tokyo Research Laboratory, Tokyo, Japan, jwhaley@alum.mit.edu

• Jim Woodcock, Oxford University, UK, Jim.Woodcock@comlab.ox.ac.uk

In closing, we would like to thank the many persons, whose help has been crucial for the success of COCV 2002. First of all, we would like to thank the organizers of ETAPS 2002, in particular, Rachid Echahed, the workshop chair of ETAPS 2002, for their help with the organization of the workshop as satellite event of ETAPS 2002. We are also grateful to Axel Dold, Werner Gabrisch, and Michael Schaarschmidt for their help as external reviewers, and to Michael Mislove, one of the Managing Editors of the ENTCS series, for his assistance with the use of the ENTCS style files. Furthermore, we would like to thank the participants of the Dagstuhl Seminar 00381: Code Optimisation: Trends, Challenges and Perspectives for their discussions. These discussions led to the idea of this workshop. Last but not least, we would like to thank the authors who submitted a contribution.     

Preface: Volume 82, Issue 2

Semantics preservation between source and target program is the commonly accepted minimum requirement to be ensured by compilers. It is the key term compiler verification and optimization are centered around. The precise meaning, however, is often only implicit. As a rule of thumb, verification tends to interpret semantics preservation in a very tight sense, not only but also to simplify the verification task. Optimization generally prefers a more liberal view in order to enable more powerful transformations otherwise excluded. The surveyor's rod of admissibility is semantics preservation, and hence the language semantics. But the adequate interpretation varies fluently with the application context (“stand-alone” programs, communicating systems, reactive systems, etc.).The aim of the workshop is to bring together researchers and practitioners working on optimizing and verifying compilation as well as on programming language design and semantics in order to plumb the mutual impact of these fields on each other, the degrees of freedom optimizers and verifiers have, to bridge the gap between the communities, and to stimulate synergies.The accepted papers discuss topics such as certifying compilation, verifying compilation, translation validation, and optimization. Chakravarty et al. present correctness proofs for constant-folding and dead code elimination based on SSA. Hartmann et al. discuss a method to annotate SafeTSA code in order to enable object resolution for dynamic objects under certain conditions. Their approach statically analyzes classes in order to determine if object resolution is possible during runtime. Berghofer and Strecker describe the mechanical verification of a compiler from a small subset of Java to JVM using Isabelle. The contribution of Alias and Barthou is concerned with algorithm recognition. It presents a preliminary approach for detecting whether an algorithm, i.e. a piece of code, is an instance of a more general algorithm template. Their approach relies on first transforming the piece of code under consideration into a system of affine recurrent equations (SARE) and then checking whether it is an instance of a SARE template. Glesner and Blech formalize the notion of computer arithmetic and develop a classification of such arithmetics. Based on this classification they prove the correctness of constant folding which isn't as obvious as it seems at first glance. Genet et al. prove the correctness of a converter from ordinary java class files to CAP (CAP is the class file format of Java Card). The proofs are conducted using the PVS theorem proving system. Hoflehner, Lavery and Sehr discuss validation techniques from Intel's IA64 compiler effort. They show how to improve the reliability of both source code and compilers themselves by means of appropriate validation and self-validation techniques.The papers in this volume were reviewed by the program committee consisting, besides the editors, of

• www.ics.uci.edu/~franz/ Michael Franz, University of California, Irvine, CA, USA

• www-2.cs.cmu.edu/~petel/index.html Peter Lee, Carnegie Mellon University, PA, USA

• research.microsoft.com/~emeijer/ Erik Meijer, Microsoft Research, Redmond, WA, USA

• web.comlab.ox.ac.uk/oucl/people/oege.demoor.html Oege de Moor, Oxford University, UK

• Robert Morgan, www.datapower.com DataPower, Cambridge, MA, USA

• www.cs.pitt.edu/~soffa/ Mary Lou Soffa, University of Pittsburgh, PA, USA

We are grateful to the following persons, whose help has been crucial for the success of COCV'03: Damian Niwinski and the organizers of ETAPS'2003 for their help with the organization of the Workshop as satellite event of ETAPS'2003; Mike Mislove, one of the Managing Editors of the ENTCS series, for his assistance with the use of the ENTCS style files.     

Preface: Volume 30, Issue 2

This volume contains the Proceedings of International Workshop on Optimization and Implementation of Declarative Programs (WOID′99). The Workshop was held in held in conjunction with the International Conference on Logic Programming ICLP′99 in Las Cruces, New Mexico, USA on the 2nd and 3rd of December, 1999.Overview:The aim of this workshop was to provide a forum where new trends, ideas and developments concerning the optimization and implementation of declarative languages could be discussed. It was especially geared towards bringing researchers from low-level compilation and high-level optimization together. Indeed, compilers and linkers are getting more and more sophisticated and employ more and more high-level optimizations, such as partial evaluation or deforestation. Researchers in high-level optimization and transformation, on the other hand, realise that low-level issues have to be taken into account in order to apply their techniques in practice. So, in this workshop we wanted to provide the possibility for these two areas to meet and accelerate their synergy.Contributions:Out of 11 submissions 8 papers were selected. To ensure a workshop character ample time was reserved for discussion and each paper was assigned a “key listener” from the program committee. This scheme was borrowed from the LOPSTR workshop series, and proved to be successful. The contributions were arranged in 3 sessions, described below.1. Implementation & Low-level OptimizationThe first paper of the session by R. Muth, S. Watterson, and S. Debray, discussed how the information that certain program variables “almost always” have a particular value (as opposed to “always” as in partial evaluation or constant folding) can and should be exploited for optimization. (For various reasons this paper is not present in this volume of ENTCS.) The other two papers of the session presented new ways of efficiently implementing CLP languages and constructs. The paper by N-F. Zhou and S. Kaneko presented an efficient (hybrid) way to compile equality constraints, while the paper by M. Gavanelli and M. Milano showed how to efficiently implement lazy domain evaluation for Constraint Satisfaction Problems.2. AnalysisThe session on analysis comprised two papers. The first one by K. Ueda developed a new linearity analysis for concurrent logic programs, with the aim of achieving compile time garbage collection. The paper by G. Puebla and M. Hermenegildo provided an encompassing and insightful overview of the important issues and problems that arise when analysing and specialising large programs decomposed into modules.3. SpecializationThe first paper of the last session, by F. Fioravanti, A. Pettorossi, and M. Proietti, presented a novel way to specialise (C)LP programs within a given context. This context allows one to describe additional specialisation constraints which are hard (or impossible) to express in earlier approaches. The next paper, by W. Vanhoof and M. Bruynooghe, dicussed how to achieve a binding-time analysis (i.e., figuring out which values and operations are already known or executable at specialisation time) for offline partial evaluation in the context of Mercury programs with modules. Finally, the paper by M. Leuschel and J. Jorgensen (presented by H. Lehmann) gave an overview of a new, fast offline partial evaluation system (called LOGEN), which can handle partially static data structures and many pure and impure features of Prolog.Further information about the workshop can be obtained at: http://www.ecs.soton.ac.uk/~mal/iclp99.woid.html.The Program Committee was composed of:Saumya Debray(University of Arizona)Bart Demoen(University of Leuven)John Gallagher(University of Bristol)Michael Leuschel (Chair)(University of Southampton)Germán Puebla(University of Madrid)Peter Stuckey(University of Melbourne)Neng-Fa Zhou(Kyushu Institute of Technology)I would like to thank the authors for their participation in the workshop and the program committee for their efforts in reviewing the papers. I also want to thank the Managing Editors of the Electronic Notes in Computer Science series, Michael Mislove, Maurice Nivat, and Christos Papadimitriou, for providing the opportunity to publish the proceedings in this series.Michael Leuschel, Guest Editor