******************************************************************* * 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 * Calls for Papers and Conference Announcements Symposium on Functional and Logic Programming Clifford Lectures and Workshop on the Mathematical Foundations of Programming Semantics Symposium on the Theory and Applications of Satisfiability Testing TABLEAUX 2002 Workshop on Complexity in Automated Deduction Workshop on Fixed Points in Computer Science Workshop on Domain Theory * Book Announcements The pi-Calculus, A Theory of Mobile Porcesses by D.Sangiorgi, D.Walker Handbook of Automated Reasoning edited by J.A.Robinson, A.Voronkov * Journals Special Issue on Proof Carrying Code of the Journal of Automated Reasoning * Position Announcement Postdoc Positions at Toronto SIXTH INTERNATIONAL SYMPOSIUM ON FUNCTIONAL AND LOGIC PROGRAMMING (FLOPS 2002) (Co-Located with ACM SIGPLAN ASIA-PEPM 2002) Call for Papers Aizu, Japan, September 15-17, 2002 http://www.ipl.t.u-tokyo.ac.jp/FLOPS2002/ * Theme. FLOPS is a forum for research on all issues concerning functional programming and logic programming. In particular, it wants to stimulate the cross-fertilization as well as integration of the two paradigms. FLOPS 2002 invites original papers in all areas of functional and logic programming, including foundations, implementations and applications. Original research papers and system descriptions are solicited. * Submission is Web-based. In order to submit a paper, authors should fill in the submission form available at http://www.ucm.es/info/flops2002/www/submit.html where more detailed instructions are given. * Important Dates Paper submission: March 1, 2002 Notification of acceptance: May 21, 2002 Final version due: June 25, 2002 * Program committee. Maria Alpuente (Spain), Wei-Ngan Chin (Singapore), Pierre Deransart (France), Moreno Falaschi (Italy), Michael Hanus (Germany), Zhenjiang Hu (Co-Chair, Japan), Jan Maluszynski (Sweden), Aart Middeldorp (Japan), Gopalan Nadathur (USA), Susumu Nishimura (Japan), Catuscia Palamidessi (USA), Mario Rodriguez-Artalejo (Co-Chair, Spain), Francesca Rossi (Italy), Harald Sondergaard (Australia), Kwangkeun Yi (Korea), Kazunori Ueda (Japan) 2002 CLIFFORD LECTURES and EIGHTEENTH?MFPS?(MFPS 18)?? ??First Announcement ? Tulane University ? New Orleans, LA USA, March 20 - 26, 2002 ? http://www.math.tulane.edu/~mfps/mfps18.html * This year's?MFPS workshop - MFPS 18 - will be held in conjunction with the 2002 Clifford Lectures, an annual lecture series sponsored by the Tulane Mathematics Department. * The Clifford Lectures?are named in honor of A. H. Clifford, noted algebraist and longtime member of the Tulane Mathematics Department. The 2002 Clifford Lecturer is Sergei N. Artemov, Gaduate Center, CUNY. The lectures will include invited talks by other participants. The lectures will take place from midday, March 20, 2002 through midday, March 23, 2002. A complete list of speakers can be found at the web site listed above. *?The Eighteenth Workshop on the Mathematical Foundations of Programming Semantics (MFPS 18) will take place at Tulane immediately following the Clifford Lectures. The invited speakers include Rajeev Alur (Penn),?Patrick Cousot (ENS), John Hatcliff (Kansas State), John Mitchell (Stanford), John Reynolds (CMU) and Doug Smith (Kestrel). In addition there will be three special sessions. The remainder to fhe program will consist of talks contributed by participants. The available slotts will be allocated on a first come - first serve basis. *?To submit an abstract for a contributed talk, send email to mfps@math.tulane.edu giving the title and a short abstract. *?More information about both meetings can be found at the MFPS 18 home page http://www.math.tulane.edu/~mfps/mfps18.html? 5TH INTERNATIONAL SYMPOSIUM ON THE THEORY AND APPLICATIONS OF SATISFIABILITY TESTING Call for Papers, SAT solvers, SAT benchmarks May 6-9, 2001, Cincinnati, Ohio, USA http://gauss.ececs.uc.edu/Conferences/SAT2002 * Topics: Several aspects of Satisfiability testing will be explored including: propositional proof systems, search techniques, relationship between BDDs and search, applications such as in formal verification, probabilistic analysis of SAT algorithms and SAT properties, upper bounds on SAT algorithm performance, specific solvers, empirical results, quantified boolean formulas, and related topics. * Invited Speakers: Edmund Clarke (Carnegie Mellon University, USA), Jo?o Marques-Silva (Inst. Superior T?cnico, Universidade T?cnica de Lisboa), Uwe Sch?ning (Universit?t Ulm, Germany) * In conjunction with the symposium: SAT Solver Competition (BDD packages welcome): see the symposium home page for details. Special Mini-Workshop on QBF: see the symposium home page for details. * For submission details, see the symposium home page. * Important Dates: Submission of extended abstracts: February 6, 2002. Submission of SAT solvers: March 6, 2002. Submission of SAT benchmarks: March 6, 2002. Decisions on extended abstracts returned: March 6, 2002. SAT Solver Bugfixes: March 27, 2002. SAT Solver Competition: Starting April 6, 2002, until the conference. Requests to participate without submission: April 10, 2002. Conference: May 6 - 9, 2002. Submission of final journal articles: May 30, 2002. * Program Committee: Dimitris Achlioptas (Microsoft Research, USA), Endre Boros (Rutcor, Rutgers University, USA), Nadia Creignou (Universit? del la M?diterran?e, Marseille, France), Joe Culberson (University of Alberta, Edmonton, Canada), Olivier Dubois (Universit? Paris 6, France), Thomas Eiter (Technische Universit?t Wien, Austria) John Franco (University of Cincinnati, USA) Ian Gent (St. Andrews University, Scotland, UK) Andreas Goerdt (Chemnitz, Germany) Edward A. Hirsch (Steklov Institute of Mathematics at St. Petersburg, Russia) Russell Impagliazzo (UC San Diego, USA) Henry Kautz (University of Washington, USA) Lefteris Kirousis (University of Patras, Greece) Hans Kleine B?ning (Universit?t Paderborn, Germany) Oliver Kullmann (Swansea, Wales, UK) Daniel Le Berre (Universit? d'Artois, France) Chu-Min Li (LaRIA, Universit? de Picardie Jules Verne, France) Hans van Maaren (University of Delft, The Netherlands) Paul W. Purdom (Indiana University, USA) Bart Selman (Cornell University, USA) Ewald Speckenmeyer (Universit?t K?ln, Germany) Allen Van Gelder (UC Santa Cruz, USA) Miroslav N. Velev (Carnegie Mellon University, USA) Toby Walsh (University of York, UK) Lintao Zhang (Princeton University, USA) TABLEAUX 2002 Call for Papers July 30 - August 1, 2002 in Copenhagen, Denmark, as part of the Federated Logic Conference FLoC'02 http://floc02.diku.dk/TABLEAUX/ * The conference invites papers concerning all aspects - theoretical foundations, implementation techniques, systems development and applications - of the mechanization of reasoning with tableaux and related methods. * All submissions must be done electronically via http://www.logic.at/TAB02/ Detailed information on submission categories can be found at http://floc02.diku.dk/TABLEAUX/cfp.html * Important dates Submission deadline: February 2, 2002 Notification of acceptance: March 29, 2002 Camera-ready copy due: May 10, 2002 * Program committee: Peter Baumgartner (U Koblenz-Landau), Bernhard Beckert (U Karlsruhe), Marcello D'Agostino (U Ferrara, Italy), Roy Dyckhof (U St Andrews), Uwe Egly (TU Vienna, co-chair), Christian Fermueller (TU Vienn, co-chair) Melvin Fitting (City U of NY), Didier Galmiche (LORIA Nancy), Rajeev Gore (ANU), Jean Goubault-Larrecq (ENS Cachan), Reiner Haehnle (Chamlers U), Ian Horrocks (U Manchester), Christoph Kreitz (Cornell), Reinhold Letz (TU of Munich), Fabio Massacci (U Siena), Neil Murray (SU of NY-Albany), Nicola Olivetti (U Torino). WORKSHOP ON COMPLEXITY IN AUTOMATED DEDUCTION (affiliated with CADE-18) July 25-26 2002 in Copenhagen, Denmark * Aim of the workshop: The Workshop on Complexity in Automated Deduction will bring together researchers who work on or have a serious interest in problems that are in the interface between automated deduction and computational complexity. The aim of the workshop is to enhance the interaction between automated deduction and computational complexity through invited and contributed talks that will present comprehensive overviews, report on state-of-the art advances, and expand the horizons of this area of research. * Invited speakers: Marco Cadoli (Universit? di Roma La Sapienza, Roma, Italy), Hubert Comon (LSV, ENS Cachan, France), Erich Gr?del (RWTH Aachen, Germany), Martin Grohe (University of Edinburgh, UK), Phokion G. Kolaitis (University of California, Santa Cruz, USA), Paliath Narendran (SUNY Albany, USA), Reinhard Pichler (Siemens AG Austria and TU Wien, Vienna, Austria), Pavel Pudl?k (Mathematical Institute, Academy of Sciences, Prague, Czech Republic), Andrei Voronkov (University of Manchester, UK) * Contributed talks: In addition to the invited presentations, there will be contributed talks. If you are interested in giving such a contributed talk, please send an abstract, preferably as a PostScript attachment, to Miki.Hermann@loria.fr no later than Friday, May 17, 2002. * Organizers: Georg Gottlob (TU Wien, Vienna, Austria), Miki Hermann (LORIA, Nancy, France), Michael Rusinowitch (LORIA, Nancy, France) * Important dates: Submission of abstracts for contributed talks: May 17, 2002 Notification of acceptance: June 6, 2002 Deadline for final versions of accepted papers: June 20, 2002 Workshop: July 25 and 26, 2002 WORKSHOP ON FIXED POINTS IN COMPUTER SCIENCE (FICS'02) (affiliated with LICS'02) Preliminary Call for Papers July 20-21, 2002, Copenhagen, Denmark http://floc02.diku.dk/FICS/ * Theme: Construction and reasoning about properties of fixed points, categorical, metric and ordered fixed point models, continuous algebras, relation algebras, fixed points in process algebras and process calculi, regular algebras of finitary and infinitary languages, formal power series, tree automata and tree languages, infinite trees, the mu-calculus and other programming logics, fixed points in relation to dataflow and circuits, fixed points and the lambda calculus, fixed points in logic programming and data bases. * Paper submission: Authors are invited to send three copies of an abstract not exceeding three pages to the PC cochair Anna Ingolfsdottir. Electronic submissions in the form of uuencoded postscript files are encouraged and can be sent to annai@cs.auc.dk. * Submissions are to be received before April 15, 2002. * Invited speakers: L. Aceto (Aalborg), D. Kozen (Cornell), A. Labella (Rome), G. Winskel (Cambridge, provisional). * Program Committee: J. Adamek (Braunschweig), R. Backhouse (Nottingham), S. Bloom (Hoboken NJ), J. Bradfield (Edinburgh), R. De Nicola (Florence), Z. Esik (cochair, Szeged), I. Guessarian (Paris), A. Ingolfsdottir (cochair, Aalborg), W. Kuich (Vienna), A. Labella (Rome), M. Mislove (Tulane), D. Niwinski (Warsaw). * Proceedings: Preliminary proceedings containing the abstracts of the talks will be available at the meeting. Final proceedings will be published after the meeting as a special issue of the journal Theoretical Informatics and Application (http://www.edpsciences.org/docinfos/ITA/). WORKSHOP ON DOMAIN THEORY (Domains VI) Call for Abstracts Birmingham, 16-19 September 2002. http://www.cs.bham.ac.uk/~wd6/ * AUDIENCE. The Workshop on Domains is aimed at computer scientists and mathematicians alike who share an interest in the mathematical foundations of computation. It will focus on domains, their applications and related topics. Previous meetings were held in Darmstadt (94,99), Braunschweig (96), Munich (97) and Siegen (98). The emphasis is on the exchange of ideas between participants similar in style to Dagstuhl seminars. * INVITED SPEAKERS. Ulrich Berger (Wales Swansea), Thierry Coquand (Goeteborg), Jimmie Lawson (Louisiana State), John Longley (Edinburgh), Dag Normann [to be confirmed] (Oslo), Prakash Panangaden (McGill), Uday Reddy (Birmingham), Thomas Streicher (Darmstadt). * SCOPE. Domain theory has had applications to programming language semantics and logics (lambda-calculus, PCF, LCF), recursion theory (Kleene-Kreisel countable functionals), general topology (injective spaces, function spaces, locally compact spaces, Stone duality), topological algebra (compact Hausdorff semilattices) and analysis (measure, integration, dynamical systems). Moreover, these applications are related - for example, Stone duality gives rise to a logic of observable properties of computational processes. Talks in any area of interaction with domain theory are welcome. * SUBMISSIONS. Abstracts will be dealt with on a first-come/ first-served basis. Please email one-page abstracts to domainsvi@cs.bham.ac.uk . Authors will hear from the programme committee within one or two weeks of submission. * DEADLINE : 30 April 2002 * PROGRAMME COMMITTEE. Martin Escardo (Birmingham), Achim Jung (Birmingham), Klaus Keimel (Darmstadt), Alex Simpson (Edinburgh). BOOK ANNOUNCEMENT The pi-Calculus, A Theory of Mobile Porcesses by Davide Sangiorgi and David Walker Cambridge University Press 2001 ISBN 0-521-78177-9 http://uk.cambridge.org/order/WebBook.asp?ISBN=0521781779 * A detailed text on the pi-calculus, a mathematical model highly suited to describing mobile systems, the components of which communicate and change their structure. * The book is written at the graduate level, assuming no prior acquaintance with the subject, and is intended for computer scientists interested in mobile systems. * See above url for ordering information BOOK ANNOUNCEMENT Handbook of Automated Reasoning edited by J. Alan Robinson and Andrei Voronkov MIT Press, 2001, ISBN two-volume set 0-262-18223-8 Vol. 1, 0-262-18221-1, Vol. 2, 0-262-18222-X http://mitpress.mit.edu/0262182238 Available in the USA and dependencies, the Philippines, and Canada only * Automated reasoning has matured into one of the most advanced areas of computer science. It is used in many areas of the field, including software and hardware verification, logic and functional programming, formal methods, knowledge representation, deductive databases, and artificial intelligence. This handbook presents an overview of the fundamental ideas, techniques, and methods in automated reasoning and its applications. The material covers both theory and implementation. In addition to traditional topics, the book covers material that bridges the gap between automated reasoning and related areas. Examples include model checking, nonmonotonic reasoning, numerical constraints, description logics, and implementation of declarative programming languages. * The book consists of eight parts. After an overview of the early history of automated deduction, the areas covered are reasoning methods in first-order logic; equality and other built-in theories; methods of automated reasoning using induction; higher-order logic, which is used in a number of automatic and interactive proof-development systems; automated reasoning in nonclassical logics; decidable classes and model building; and implementation-related questions. * Ordering information. See the URL above. SPECIAL ISSUE OF THE JOURNAL OF AUTOMATED REASONING Proof-Carrying Code Call for Papers http://www.site.uottawa.ca/~afelty/jar-pcc/ * Topics. Proof-carrying code and related approaches which use formal reasoning to enhance safety and reliability of software. Original results and study of tools and methods for proof generation, proof checking, and their integration with code generation/compilation. * Submission. Manuscripts should be unpublished works and not submitted elsewhere. Revised and enhanced versions of papers published in conference proceedings that have not appeared in archival journals are eligible for submission. All submissions will be reviewed according to the usual standards of scholarship and originality. The deadline for submissions is February 22, 2002. * Guest editor. Amy Felty (afelty@site.uottawa.ca). POSTDOC POSITIONS AT TORONTO Department of Computer Science University of Toronto * The theory group is offering a number of postdoctoral fellowships in the areas of computational complexity, combinatorics, graph theory, and distributed systems. The fellowships are for one year, beginning September, 2002, with a possible extension to two years. Candidates should send applications to Steve Cook (sacook@cs.toronto.edu) including a CV, a list of publications, a statement of research interests, and a list of referees. * Applications are expected by 15 January, 2002.