Newsletter 89 December 5, 2003 ******************************************************************* * Past issues of the newsletter are available at http://www.lfcs.informatics.ed.ac.uk/lics/newsletters/ * Instructions for submitting an announcement to the newsletter can be found at http://www.lfcs.informatics.ed.ac.uk/lics/newsletters/inst.html ******************************************************************* TABLE OF CONTENTS * CONFERENCES AND WORKSHOPS LICS 2004 - Call for Papers ICALP 2004 - Call for Papers WRS'04 - Call for Papers CAV'04 - Call for Papers WITS'04 - Call for Papers ACSD'04 - Call for Papers WS-FM 2004 - Call for Papers CMCS'04 - Call for papers SEFM 2004 - Call for Papers MPC2004 - Call for Papers * SUMMER/WINTER SCHOOLS EWSCS'04 - Call for Participation * BOOK ANNOUNCEMENTS Computability Theory - S. Barry Cooper Verification of Reactive Systems - Klaus Schneider Logic for Concurrency and Synchronisation - Ruy J.G.B. de Queiroz (editor) Logic and Complexity - Richard Lassaigne and Michel de Rougemont * VACANCIES Postdoc and PhD positions at CWI, Amsterdam 19TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2004) (co-located with ICALP 2004) Turku, Finland, July 14-17, 2004 http://www.lfcs.informatics.ed.ac.uk/lics/ Call for Papers * The LICS Symposium is an annual international forum on theoretical and practical topics in computer science that relate to logic in a broad sense. We invite submissions on that theme. Suggested, but not exclusive, topics of interest for submissions include: automata theory, automated deduction, categorical models and logics, concurrency and distributed computation, constraint programming, constructive mathematics, database theory, domain theory, finite model theory, proof theory, formal aspects of program analysis, formal methods, hybrid systems, lambda and combinatory calculi, linear logic, logical aspects of computational complexity, logics in artificial intelligence, logical representation of knowledge, logics of programs, logic programming, modal and temporal logics, model checking, programming language semantics, reasoning about security, rewriting, specifications, type systems and type theory, and verification. * Authors are required to submit electronically a paper title and a short abstract of about 100 words before submitting the extended abstract of the paper. Titles & Short Abstracts Due : January 26, 2004 Extended Abstracts Due : February 2, 2004 Author Notification : March 27, 2004 Camera-ready Papers Due : April 25, 2004 All deadlines are firm; late submissions will not be considered. Detailed information about electronic paper submission will be posted at the LICS website. * LICS 2004 will have a session of short (5--10 minutes) presentations. This session is intended for descriptions of work in progress, student projects, and relevant research being published elsewhere; other brief communications may be acceptable. Submissions for these presentations, in the form of short abstracts (1 or 2 pages long), should be entered at the LICS 2004 submission site between March 27th and April 4th, 2004. Authors will be notified of acceptance or rejection by April 17th, 2004. * An award in honor of the late S.C. Kleene will be given for the best student paper, as judged by the program committee. For a submission to be eligible, the research presented in the paper must have been carried out while all authors were full-time students. The program committee may decline to make the award or may split it among several papers. * As in previous years, there will be a number of workshops affiliated with LICS 2004; information will be posted at the LICS website. * Program committee: Rajeev Alur, Andrew Appel, Albert Atserias, Franz Baader, Samuel Buss, Roberto Di Cosmo, Gilles Dowek, Harald Ganzinger (chair), Martin Hofmann, Achim Jung, Kim Larsen, Leonid Libkin, Rocco de Nicola, Damian Niwinski, Prakash Panangaden, Albert Rubio, Vitaly Shmatikov, Moshe Vardi, Helmut Veith, Andrei Voronkov * Invited speakers: LICS: S. Abramsky (O. Oxford), D. Sangiorgi (U. di Bologna), I. Walukiewicz (U. Bordeaux), Joint ICALP/LICS: R. Harper (Carnegie Mellon), A. Razborov (Princeton & Moscow), M. Yannakakis (Stanford). 31ST INTL COLLOQ ON AUTOMATA, LANGUAGES AND PROGRAMMING (ICALP 2004) (co-located with LICS 2004) Turku, Finland, July 12-16, 2004 http://www.math.utu.fi/icalp04/ Call for Papers * Papers presenting original research on all aspects of theoretical computer science are sought. Typical but not exclusive topics of interest are as follows: TRACK A: Algorithmic aspects of parallel and distributed computing; algorithms and data structures; algorithms and models for large networks; algorithms for computationally hard problems; automata theory and formal languages; bioinformatics; computational complexity; combinatorics and structures in Computer Science; cryptography; machine learning; molecular computing, neural and evolutionary algorithms; proof complexity; quantum computing. TRACK B: Algebraic and categorical models; applications of automata in logic; concurrency, mobility and distributed systems; databases, semi-structured data and finite model theory; logics and their applications; principles of programming languages; program logics, formal methods and model checking; security analysis and verification; semantics of programming languages; specification, refinement and verification; type systems and typed calculi. * Submissions of max 12 pages to be submitted via the conference web site. Accepted papers will be published in Springer LNCS. * Submission deadline: February 8, 2004. Notification: March 31, 2004 * Program committees: TRACK A: A. Atserias, Barcelona (ES), G. Brodal, Aarhus (DK), J. Cassaigne, Marseille (FR), J. D?az, Barcelona (ES), chair, R. Fleischer, Hong Kong (HK), H. Gabow, Boulder (US), L. Goldberg, Warwick (UK), J. Hromkovic, Aachen (DE), G. Italiano, Roma (IT), T. Jiang, Riverside (US), C. Kaklamanis, Patras (GR), J. Kari, Turku (FI), C. Moore, Santa Fe (US), P. Pudlak, Prague (CZ), P. Raghavan, Verity, Stanford (US), M. Santha, Paris (FR), B. Voecking, Dortmund (DE), G. Woeginger, Twente (NL), M. Yung, Columbia U. (US). TRACK B: R.-J. Back, Turku (FI), P.-L. Curien, Paris (FR), A. Gordon, Microsoft, Cambridge (UK), S. Hayashi, Kobe (JP), T. Henzinger, Berkeley (US), M. Hofmann, Munich (DE), B. Jacobs, Nijmegen (NL), E. Moggi, Genova (IT), J. Parrow, Uppsala (SE), C. Palamidessi, University Park, Penn. (US), B. Pierce, Philadelphia (US), A. Rabinovich, Tel Aviv (IL), D. Sannella, Edinburgh (UK), chair, W. Thomas, Aachen (DE), I. Walukiewicz, Bordeaux (FR). * Invited speakers: ICALP: P. Flajolet (INRIA), M. Henzinger (Google), M. Hofmann (Munich), W. Rytter (Warsaw & NJIT). Joint ICALP/LICS: R. Harper (Carnegie Mellon), A. Razborov (Princeton & Moscow), M. Yannakakis (Stanford). WORKSHOP ON REDUCTION STRATEGIES IN REWRITING AND PROGRAMMING (WRS'04) June 2 2003, Aachen, Germany http://www-i2.informatik.rwth-aachen.de/WRS04/ Call for Papers * Papers are solicited on all aspects of reduction strategies in rewriting and programming. * Deadline: March 17 2004 * For more information see Web page. COMPUTER AIDED VERIFICATION (CAV'04) July 13-17 2004, Omni Parker House Hotel, Boston, USA http://www.dcs.warwick.ac.uk/CAV Call for Papers * CAV'04 conference is the 16th in a series dedicated to the advancement of the theory and practice of computer-assisted formal analysis methods for software and hardware systems. The conference covers the spectrum from theoretical results to concrete applications, with an emphasis on practical verification tools and the algorithms and techniques that are needed for their implementation. * Deadline (strict): January 23, 2004 * For more information see Web page WORKSHOP ON ISSUES IN THE THEORY OF SECURITY (WITS'04) April 3-4 2004, Barcelona, Spain Co-located with ETAPS'04 http://www.dsi.unive.it/IFIPWG1_7/wits2004.html Call for Papers * WITS is the offical workshop organised by the IFIP WG 1.7 on "Theoretical Foundations of Security Analysis and Design", established to promote the investigation on the theoretical foundations of security, discovering and promoting new areas of application of theoretical techniques in computer security and supporting the systematic use of formal techniques in the development of security related applications. The members of WG hold their annual workshop as an open event to which all researchers working on the theory of computer security are invited. This is the fourth workshop of the series, and is organised in cooperation with ACM SIGPLAN and GI working group FoMSESS. * Extended abstracts of work (accepted after selection and) presented at the Workshop are collected and distributed to the participants. There will be no formally published proceedings; however, selected papers will be invited for submission to a special issue of the Journal of Computer Security. * Deadline: 15 December 2003 * For more information see Web page APPLICATION OF CONCURRENCY TO SYSTEM DESIGN (ACSD'04) June 16-18 2004, Hamilton, Canada http://acsd.mcmaster.ca/ Call for Papers * The International Conference on Application of Concurrency to System Design (ACSD) serves as a forum for disseminating theoretical results and advanced methods and tools for the design of complex concurrent systems. While there are a few success stories in the field, there is still a strong need to bring theory and practice closer together. The conference aims at cross-fertilizing both types of research. * Deadline for submissions: 19 December, 2003 * For more information see Web page 1st International Workshop on Web Services and Formal Methods (WS-FM 2004) February 23 2004, Pisa, Italy http://www.cs.unibo.it/~lucchi/ws-fm04/ Call for Papers * The aim of the workshop is to bring together researchers working on Web Services and Formal Methods in order to activate a fruitful collaboration in this direction of research. This, potentially, could also have a great impact on the current standardization phase of Web Service technologies. * Deadline: December 15, 2003 * For more information see Web page COALGEBRAIC METHODS IN COMPUTER SCIENCE (CMCS 2004) March 27-29, 2004, barcelona, Spain Co-located with ETAPS'04 http://www.iti.cs.tu-bs.de/~cmcs/ Call for Papers * During the last few years, it is becoming increasingly clear that a great variety of state-based dynamical systems, like transition systems, automata, process calculi and class-based systems can be captured uniformly as coalgebras. Coalgebra is developing into a field of its own interest presenting a deep mathematical foundation, a growing field of applications and interactions with various other fields such as reactive and interactive system theory, object oriented and concurrent programming, formal system specification, modal logic, dynamical systems, control systems, category theory, algebra, analysis, etc. The aim of the workshop is to bring together researchers with a common interest in the theory of coalgebras and its applications. * Deadline for submission: January 1, 2004 * For more information see Web page SOFTWARE ENGINEERING AND FORMAL METHODS (SEFM 2004) Beijing, China 26-30 September 2004 http://www.iist.unu.edu/SEFM2004 Call for Papers * The aim of the conference is to bring together practitioners and researchers from academia, industry and government to advance the state of the art in formal methods, to scale up their application in software industry and to encourage their integration with practical engineering methods. * Important dates: Submission deadline for abstract: 29 March 2004 Submission deadline for papers: 05 April 2004 Notification of acceptance: 18 June 2004 Camera-ready version due: 12 July 2004 Tutorials and workshops: 26-27 September 2004 SEFM 2004 in Beijing, China: 28-30 September 2004 * For more information see Web page 7TH INTERNATIONAL CONFERENCE ON MATHEMATICS OF PROGRAM CONSTRUCTION (MPC2004) (in conjunction with AMAST 2004) Stirling, Scotland, UK, 12--14 July, 2004 http://www.cs.cornell.edu/Projects/MPC2004 Call for Papers * Theme. The development of mathematical principles and techniques that are demonstrably useful in the process of constructing computer programs, whether implemented in hardware or software; techniques that combine precision with conciseness, enabling programs to be constructed by formal calculation. We welcome contributions to programming methodology, to programming paradigms and to language design; theoretical contributions are welcome provided their relevance to program construction is evident, and discussion of applications is welcome provided the mathematical basis is evident. * Submission of full papers in Postscript or PDF by email to patwell@cs.cornell.edu * Submission Deadline: 31st January, 2004 * Program committee. Roland Backhouse, Stephen Bloom, Eerke Boiten, Jules Desharnais, Thorsten Ehm, Jeremy Gibbons, Ian Hayes, Eric Hehner, Johan Jeuring, Dexter Kozen (chair), Rustan Leino, Hans Leiss, Christian Lengauer, Lambert Meertens, Bernhard Moeller, David Naumann, Alberto Pardo, Georg Struth, Jerzy Tiuryn, Mark Utting. 9th ESTONIAN WINTER SCHOOL IN COMPUTER SCIENCE (EWSCS'04) Call for Participation Palmse, Estonia, 29 Feb - 5 March 2004 http://www.cs.ioc.ee/yik/schools/win2004/ * EWSCS is a series of regional-scope international winter schools held annually in Estonia. The main objective of EWSCS is to expose Estonian, Baltic, and Nordic graduate students in computer science (but also interested students from elsewhere) to frontline research topics usually not covered within the regular curricula. The subject of the schools is general computer science, with a bias towards theory, this comprising both algorithms, complexity and models of computation, and semantics, logic and programming theory. The working language of the schools is English. * The schools' scientific programme consists of short courses by renowned specialists and a student session. The course list for EWSCS'04 is the following: - Sergei Artemov (City University of New York, USA): [Explicit Provability and Constructive Semantics] - Rusins Freivalds (University of Latvia, Riga, Latvia): Unreasonable Effectiveness of Classical Mathematics in Computer Science - Achim Jung (University of Birmingham, UK): Stone Duality and Program Logics - Moni Naor (Weizmann Institute, Rehovot, Israel): Cryptography and Privacy-Preserving Operations - Madhu Sudan (MIT / Radcliffe Institute, Cambridge, MA, USA): Algorithmic Introduction to Coding Theory * The purpose of the student session is to give students an opportunity to present their own ongoing work (typically, thesis work) and get feedback. Registrants to EWSCS'04 are invited to propose short talks (20 min) or posters. The selection will be based on abstracts of 150-400 words. * Deadline for registration and submission of abstracts of student talks/posters: 16 Jan 2004. Notification of acceptance: 30 Jan 2004. BOOK ANNOUNCEMENT Computability Theory S. Barry Cooper Chapman Hall/CRC Mathematics Series, Volume 26, 2003, ISBN: 1584882379 http://www.crcpress.com/ * Written by a leading researcher, Computability Theory provides a concise, comprehensive, and authoritative introduction to contemporary computability theory, techniques, and results. The basic concepts and techniques of computability theory are placed in their historical, philosophical and logical context. This presentation is characterized by an unusual breadth of coverage and the inclusion of advanced topics not to be found elsewhere in the literature at this level. * The book includes both the standard material for a first course in computability and more advanced looks at degree structures, forcing, priority methods, and determinacy. The final chapter explores a variety of computability applications to mathematics and science. * Computability Theory is an invaluable text, reference, and guide to the direction of current research in the field. Nowhere else will you find the techniques and results of this beautiful and basic subject brought alive in such an approachable and lively way. * Ordering information. See publisher's URL above. BOOK ANNOUNCEMENT Verification of Reactive Systems Klaus Schneider Springer Verlag, 2003, ISBN 3-540-00296-0 http://rsg.informatik.uni-kl.de/VeReSys * This book considers the most popular logics for specification and verification of reactive systems. In particular, the relationships and verification procedures of the propositional mu-calculus, omega-automata, temporal logics, and (monadic) predicate logics are covered in full detail. The book has a special emphasis on algorithms that are listed as detailed pseudo-code programs. This makes the book particularly useful for those who want to implement modern verification procedures. Most results are given with detailed proofs, so that the presentation is self-contained. This book is targeted to advanced students, lecturers, and researchers in the area. * Course materials (slides and exercises) based on the book will be made available before/during the next summer term. A preliminary German version can be found under the above URL. * A public domain verification tool (Equinox) will be made available during the next year. BOOK ANNOUNCEMENT Logic for Concurrency and Synchronisation Ruy J.G.B. de Queiroz (editor) Volume 18 of the series "Trends in Logic" Kluwer Academic Publishers, Dordrecht Hardbound, ISBN 1-4020-1270-5, xxi+284pp July 2003 http://www.wkap.nl/prod/b/1-4020-1270-5 * From the Foreword (by Johan van Benthem): The individual chapters of this book show the state of the art in current investigations of process calculi such as linear logic, pi-calculus, and mu-calculus - with mainly two major paradigms at work, namely, linear logic and modal logic. These techniques are applied to the title themes of concurrency and synchronisation, but there are also many repercussions for topics such as the geometry of proofs, categorial semantics, and logics of graphs. Viewed together, the chapters also offer exciting glimpses of future integration, as the reader moves back and forth through the book. Obvious links include modal logics for proof graphs, labeled deduction merging modal and linear logic, Chu spaces linking proof theory and model theory, and bisimulation-style equivalences as a tool for analyzing proof processes. The combination of approaches and the pointers for further integration in this book also suggests a grander vision for the field. In classical computation theory, Church's Thesis provided a unification and driving force. Likewise, modern process theory would benefit immensely from a synthesis bringing together paradigms like modal logic, process algebra, and linear logic - with their currently still separate worlds of bisimulations, proofs, and normalisation. If this Grand Synthesis is ever going to happen, books like this are needed! BOOK ANNOUNCEMENT Logic and Complexity Richard Lassaigne and Michel de Rougemont Springer-Verlag, 2003, ISBN 1-85233-565-3 http://www.springeronline.com/1-85233-565-3 * Logic and Complexity looks at basic logic as it is used in Computer Science, and provides students with a logical approach to Complexity theory. With plenty of exercises, this book presents classical notions of mathematical logic, such as decidability, completeness and incompleteness, as well as new ideas brought by complexity theory such as NP-completeness, randomness and approximations, providing a better understanding for efficient algorithmic solutions to problems. Divided into three parts, it covers: - Model Theory and Recursive Functions - introducing the basic model theory of propositional, 1st order, inductive definitions and 2nd order logic. Recursive functions, Turing computability and decidability are also examined. - Descriptive Complexity - looking at the relationship between definitions of problems, queries, properties of programs and their computational complexity. - Approximation - explaining how some optimization problems and counting problems can be approximated according to their logical form. Logic is important in Computer Science, particularly for verification problems and database query languages such as SQL. *Ordering Information: http://www.springeronline.com/1-85233-565-3 POSTDOC AND PHD POSITIONS AT CWI, AMSTERDAM http://www.cwi.nl/sen3 * The Coordination and Component Based Software group in SEN3 at CWI has two open positions for: (1) a postdoc for a period of four years, and (2) a PhD student (OIO) for four years. Both positions are within the project number 600.065.120.03N02 Compositional Construction of Component Connectors (C-Quattro), recently funded by the NWO (the Dutch government's funding agency for academic scientific research), with F. Arbab (CWI) and J. Rutten (CWI and VUA) as Principal Investigators. The project C-Quattro is in fact a collaboration of SEN3 at CWI with the Section Theoretical Computer Science at the Free University of Amsterdam (VUA). The postdoc will be employed by CWI; the PhD student will be employed by the VUA but will spend part of his or her time at CWI. * For more information on these vacancies, contact either of the PIs: F. Arbab, telephone +31-20-5924056, e-mail Farhad.Arbab@cwi.nl J. Rutten, telephone +31-20-592-4116, email Jan.Rutten@cwi.nl
Back to the LICS web page.