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 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     

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 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 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 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 70, Issue 1

This paper defines reduction on derivations in the strict intersection type assignment system of [2], by generalising cutelimination, and shows a strong normalisation result for this reduction. Using this result, new proofs are given for the approximation theorem and the characterisation of normalisability using intersection types.     

Preface: Volume 72, Issue 3

This volume contains the Proceedings of the Workshop on Graph Transformation and Visual Modelling Techniques (GT-VMT 2002). The Workshop was held in Barcelona, Spain, on October 11 and 12, 2002, as satellite event of the First International Conference on Graph Transformation (ICGT 2002).

Background

Diagrammatic notations have accompanied the development of technical and scientific disciplines in fields as diverse as mechanical engineering, quantum physics, category theory, and software engineering. In general, diagrammatic notations allow the construction of images associated with an interpretation based on considering as significant some well-defined spatial relations among graphical tokens. These tokens either derive from conventional notations employed in a user community or are elements specially designed to convey some meaning. The notations serve the purpose of defining the (types of) entities one is interested in and the types of relations among these entities. Hence, types must be distinguishable from one another and no ambiguity may arise as to their interpretation. Moreover, the set of spatial relations to be considered must be clearly defined, and the holding of any relation among any set of elements must be decidable.The evolution of diagrammatic notations usually follows a pattern that, from their usage as illustrations of sentences written in some formal or natural language, leads to the definition of "modelling languages". These languages are endowed with rules for the construction of "visual sentences" from some elementary graphical components, and for interpreting the meaning of these sentences with respect to the modeled domain, up to rules for mapping the behaviour of the modeled systems onto the behaviour of the visual elements in the model.

Workshop Objectives

As diagrammatic notations, such as UML, become widespread in software engineering and visual end user environments, there is an increasing need of formal methods to precisely define the syntax and semantics of such diagrams. In particular, when visual models of systems or processes constitute executable specifications of systems, not only is a non-ambiguous specifications of their static syntax and semantics needed, but also an adequate notion of diagram dynamics. Such a notion must establish links (e.g., morphisms) which relate diagram transformations and transformations of the objects of the underlying domain. The field of Graph Grammars and Graph Transformation Systems has contributed much insight into the solution of these problems, but also other approaches (e.g., meta modelling, constraint-based and other rule-based systems), have been developed to tackle specific issues.The workshop has followed in the line of successful workshops on Graph Transformations and Visual Modelling Techniques, which were before held as satellite events of ICALP'00 and ICALP'01. It has gathered researchers working with different methodologies to discuss the relative merits and weaknesses of the different approaches to problems such as diagram parsing, diagram transformation, integrated management of syntactic and semantic aspects, tool support for working with visual models. The focus has been on methodological aspects rather than on particular technical aspects.

Program Committee

The papers in this volume were reviewed by the program committee consisting of

Paolo Bottoni (Co-Chair)	Department of Computer Science, University of Rome 'La Sapienza', Italy
Andrea Corradini	Computer Science Department, University of Pisa, Italy
Gregor Engels	Mathematics/Computer Science Department, University of Paderborn, Germany
Reiko Heckel	Mathematics/Computer Science Department, University of Paderborn, Germany
Stuart Kent	Computing Laboratory, University of Kent, UK
Bernd Meyer	School of Computer Science and Software Engineering, Monash University, Melbourne, Australia
Mark Minas (Co-Chair)	Department of Computer Science, University of the Federal Armed Forces, Munich, Germany
Francesco Parisi Presicce	Department of Computer Science, University of Rome 'La Sapienza', Italy
Mauro Pezzè	Department of Information Sciences, University of Milan Bicocca, Italy
Grzegorz Rozenberg	Institute of Advanced Computer Science, Leiden University, The Netherlands
Gabriele Taentzer	Computer Science Department, Technical University of Berlin, Germany

Full-size table

Workshop program

The workshop was scheduled for one and a half day and included a session with an invited talk by Martin Gogolla as well as 12presentations of papers in four regular sessions on Geometry and Visualization, on Frameworks and Tools, on Euler/Venn Diagrams, and on Components, Models, and Semantics.

Joint Session

The workshop featured a special session on Case Studies for Visual Modelling Techniques held jointly with the Workshop onSoftware Evolution Through Transformations (SET 2002).This session was part of the work carried out under the European research training network SegraVis (for Syntactic and Semantic Integration of Visual Modelling Techniques) with the objective to employ, evaluate, and improve visual modelling techniques in specific domains, including (but not limited to)

modelling support for software evolution and refactoring

modelling of component-based software architectures

specification of applications with mobile soft- and hardware

Beside a general discussion of these objectives, the session consisted in presentations of three submitted case studies and position statements by the SegraVis objective coordinators.

Acknowledgement

This workshop was supported by the European research training network Segra Vis.     

Preface: Volume 82, Issue 6

Component-based systems are increasingly used in software development. The lack of information about internals at different development stages and the need for optimizing verification and validation require new approaches to test and analysis.TACoS 2003 provided a forum for discussing techniques, tools, and experiences on testing, analysis and design for testability of components, component based systems, and configurable products. This year, the focus of TACoS was on heterogeneous, modular and configurable embedded systems that share hardware and software resources and are available in several versions.We received contributions from Australia, Brazil, China, Germany, Greece, Italy, Japan, Poland, Spain, Sweden, the United Kingdom, and the United States, witnessing a strong international interest in the topic. Thanks to the high quality of the submissions, the Program Committee was able to select 19 papers representing the state-of-art in the area.The workshop was organized as discussion sessions around four major topics: Testing Component Based Systems, Configurability, Analysis and Test of Component Based Real-Time Systems, Specification and Design for Testability. Each topic has been introduced by a brief presentation of related papers followed by a discussion among participants.The workshop was promoted and organized by the Quack (A Platform for the Quality of New Generation Integrated Embedded Systems) project, an Italian project sponsored by the Ministry of University, Research and Education.The success of the workshop stimulated the organization of new events. TACoS 2004 will be held in Barcelona as a satellite event of ETAPS 2004. We hope that the core community that met in Warsaw will grow in Barcelona. The official TACoS web site (www.lta.disco.unimib.it/tacos/)will keep updated information about the upcoming events.

Acknowledgments

We would like to thank all authors who submitted their work for presentation at TACoS and participated to the fruitful discussion. We express our gratitude to the Organizing and the Steering Committees of ETAPS, who gave us an excellent support. A special thank to the members of the Program Committee and the many reviewers that supported a smooth and exciting reviewing process. Among all people that contributed to TACoS, we would like to mention Giovanni Denaro and Leonardo Mariani who took care of a variety of aspects of the organization and gave a determinant contribution to the success of the event.Milan, April 2003 - Mauro Pezzè

Program Committee

Marco Di Natale - Scuola Superiore Sant'Anna di Pisa (Italy)Alessandro Fantechi - Università degli Studi di Firenze (Italy)Gerhard Fohler - Malardalen University (Sweden)Frank van der Linden - University of Amsterdam (The Netherlands)Angelo Morzenti - Politecnico di Milano (Italy)Elie Najm - Ecole Nationale Superieure des Telecommunications (France)Mauro Pezzè - Università degli Studi di Milano Bicocca (Italy)Paolo Prinetto - Politecnico di Torino (Italy)Michal Young - University of Oregon (USA)Alex Orailoglu - University of California in San Diego (USA)Chantal Robach - Ecole Superieure d'Ingenieurs en Systemes Industriels Avances (France)     

Preface: Volume 86, Issue 3

This volume contains selected papers presented at the International Workshop on Functional and (Constraint) Logic Programming (WFLP 2003), held in Valencia (Spain) during June 12-13, 2003, at the Federated Conference on Rewriting, Deduction and Programming (RDP 2003). WFLP 2003 is the twelfth in the series of international meetings aimed at bringing together researchers interested in functional programming, (constraint) logic programming, as well as their integration. It promotes the cross-fertilizing exchange of ideas and experiences among researches and students from the different communities interested in the foundations, applications, and combinations of high-level, declarative programming languages and related areas. Previous WFLP editions have been held in Grado (Italy), Kiel (Germany), Benicàssim (Spain), Grenoble (France), Bad Honef (Germany), Schwarzenberg (Germany), Marburg (Germany), Rattenberg (Germany), and Karlsruhe (Germany).The Program Committee of WFLP 2003 selected, from all contributions presented at the workshop (which had been reviewed before the workshop), papers for inclusion into this special issue. The authors of all selected papers prepared revised versions after the workshop which were refereed again in order to ensure a high scientific quality. This volume contains the finally accepted versions based on this review process. In addition to the selected papers, the scientific program included invited lectures by Michael Rusinowitch (LORIA-INRIA-Lorraine, France) and Jan Maluszynski (Linköping University, Sweden).The program committee of WFLP 2003 consisted of

María Alpuente	(Technical University of Valencia, Spain)
Sergio Antoy	(Portland State University, USA)
Annalisa Bossi	(Università Ca' Foscari di Venezia, Italy)
Olaf Chitil	(University of York, UK)
Rachid Echahed	(Institut IMAG, France)
Sandro Etalle	(University of Twente, The Netherlands)
Moreno Falaschi	(Università di Udine, Italy)
Michael Hanus	(CAU Kiel, Germany)
Yukiyoshi Kameyama	(University of Tsukuba, Japan)
Herbert Kuchen	(University of Muenster, Germany)
Michael Leuschel	(University of Southampton, UK)
Juan José Moreno-Navarro	(Universidad Politécnica de Madrid, Spain)
Ernesto Pimentel	(University of Málaga, Spain)
Mario Rodríguez-Artalejo	(Universidad Complutense de Madrid, Spain)
Germán Vidal	(Technical University of Valencia, Spain)

Full-size table

Organizing committee: Elvira Albert, Santiago Escobar, César Ferri, José Hernández, Carlos Herrero, Pascual Julián, Marisa Llorens, Ginés Moreno, Javier Oliver, Josep Silva, Germán Vidal, and Alicia VillanuevaAdditional referees: Elvira Albert, Zena Ariola, Demis Ballis, Bernd Brassel, Ricardo Corin, Agostino Dovier, Francisco Durán, Santiago Escobar, José Gallardo, Raffaella Gentilini, Angel Herranz, Teresa Hortalá-González, Zhenjiang Hu, Frank Huch, Pascual Julián, Christoph Lembeck, Pablo López, Salvador Lucas, Massimo Marchiori, Julio Mariño, Yasuhiko Minamide, Angelo Montanari, Ginés Moreno, Roger Müller, Susana Muñoz, Salvatore Orlando, Carla Piazza, Femke van Raamsdonk, María José Ramírez, Guido Sciavicco, Clara Segura, Jan-Georg Smaus, Andrew Tolmach, Alberto Verdejo, and Alicia Villanueva.Sponsoring institutions:Departamento de Sistemas Informáticos y Computación, Universidad Politécnica de Valencia, Generalitat Valenciana, Ministerio de Ciencia y Tecnología, European Association for Theoretical Computer Science, European Association for Programming Languages and Systems, CologNET: A Network of Excellence in Computational Logic, and APPSEM Working Group.I would like to thank the invited speakers for their willingness in accepting our invitation. I would also like to thank all the members of the Program Committee and all the referees for their careful work in the review and selection process. Many sincere thanks to all authors who submitted papers and to all conference participants. I gratefully acknowledge all the institutions and corporations who have supported this workshop. Furthermore, I would like to thank Michael Mislove, Managing Editor of the ENTCS series, for making this special issue possible. Finally, I express my gratitude to all members of the local Organizing Committee whose work has made the workshop possible.November 6, 2003Germán Vidal