Newsletter 95
October 18, 2004

*******************************************************************
* 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 2005 - Call for Papers
  LICS 2005 - Call for Workshop Proposals
  RTA 2005 - Call for Papers
  TLCA 05 - Call for Papers
  CAV 2005 - Call for Papers
  BCTCS 2005 - Announcement
  LOGIC COLLOQUIUM 2005 - Call for Abstracts and Participation
  VISSAS 2005 - Call for Papers
  COORDINATION 2005 - Call for Papers
  ICFEM 2004 - Call for Participation
* JOURNALS
  Journal of Automated Reasoning - Special Issue on Automated Reasoning for
    Security Protocol Analysis
* BOOK ANNOUNCEMENTS
  Logic Colloquium '99 - J. van Eijck, V. van Oostrom, A. Visser eds.
  Logic in Computer Science (2nd Edition) - M. Huth and M. Ryan
* VACANCIES
  Phd or Postdoc Position at HU Berlin
* PRIZES
  Nominations Sought for Nevanlinna Prize


TWENTIETH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2005)
  Chicago, Illinois, June  26th-29th, 2005
  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 broadly
  construed.  We invite submissions on topics that fit under that rubric.
  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, formal aspects of program analysis, formal methods, hybrid systems,
  lambda and combinatory calculi, linear logic, logical aspects of
  computational complexity, logics in artificial intelligence, logics of
  programs, logic programming, modal and temporal logics, model checking,
  probabilistic systems, process calculi, programming language semantics,
  reasoning about security, rewriting, specifications, type systems and type
  theory, and verification.  We welcome submissions in emergent areas, such as
  bioinformatics and quantum computation, if they have a substantial
  connection with logic.
* Authors are required to submit a paper title and a short abstract
  of about 100 words before submitting the extended abstract of the
  paper. All submissions will be electronic.
    Titles & short abstracts due: 5th January 2005
    Extended abstracts due: 10th January 2005
* Program committee: Jiri Adamek, Luca de Alfaro, Andrei Bulatov,
  Hubert Comon-Lundh, Philippa Gardner, Martin Grohe, Neil Immerman,
  Marta Kwiatkowska, Maurizio Lenzerini, Guy McCusker, Larry Moss,
  Prakash Panangaden (chair), Frank Pfenning, Toniann Pitassi,
  Uday Reddy, Thomas Schwentick, Peter Selinger, N. Shankar,
  Igor Walukiewicz
* For more information see LICS website



TWENTIETH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2005)
  Chicago, Illinois, June  26th-29th, 2005
  Workshop dates: June 25, 2005  and June 30-July 1, 2005
  http://www.lfcs.informatics.ed.ac.uk/lics/
  Call for Workshop Proposals
* The Twentieth IEEE Symposium on Logic In Computer Science (LICS 2005)
  will be held in Chicago, Illinois, USA, June 26-29, 2005. The organizers
  have made arrangements for pre- and post-LICS workshops to be run in
  conjunction with the main conference.  Possible dates are June 25
  (the day before LICS) and June 30 and July 1 (the two days after LICS).
* Researchers and practitioners are invited to submit proposals for
  workshops on topics relating logic - broadly construed - to computer
  science or related fields. Typically, LICS workshops feature a number
  of invited speakers and a smaller number of contributed presentations.
  LICS workshops do not produce formal proceedings. However, in the past
  there have been  special issues of journals based in part on certain
  LICS workshops.
* Proposals are due November 15, 2004 and should be submitted
  electronically to:
    Philip Scott
    Workshops Chair,  LICS 2005
    Email: phil@site.uottawa.ca
* For more information see LICS website



INTERNATIONAL CONFERENCE ON REWRITING TECHNIQUES AND APPLICATIONS (RTA 2005)
  (affiliated with RDP'05)
  Call for Papers
  Nara, Japan, April 19 - 21, 2005
  http://www-i2.informatik.rwth-aachen.de/RTA05/
* Theme: All aspects of rewriting. Typical areas of interest include (but are
  not limited to):
  - Applications: case studies; rule-based (functional and logic) programming;
    symbolic and algebraic computation; theorem proving; system synthesis and
    verification; proof checking.
  - Foundations: matching and unification; narrowing; completion techniques;
    strategies; constraint solving; explicit substitutions; tree automata.
  - Frameworks: string, term, and graph rewriting; lambda-calculus and
    higher-order rewriting; proof nets; constrained rewriting/deduction;
    categorical and infinitary rewriting.
  - Implementation: compilation techniques; parallel execution; rewriting
    tools.
  - Semantics: equational logic; rewriting logic.
* Submission categories include regular research papers and system
  descriptions. Also problem sets and submissions describing interesting
  applications of rewriting techniques will be very welcome.
  Electronic submissions are strongly encouraged.
* Submission deadline: November 12, 2004 for abstracts; then November 19, 2004
  for full papers. These are strict deadlines! See the conference web page
  for details.
* Program committee: Franz Baader (Dresden), Mariangiola Dezani (Torino),
  Juergen Giesl (Aachen) (Chair), Bernhard Gramlich (Vienna), Florent
  Jacquemard (Cachan), Claude Kirchner (Nancy), Pierre Lescanne (Lyon), Aart
  Middeldorp (Innsbruck), Hitoshi Ohsaki (Amagasaki), Vincent van Oostrom
  (Utrecht), Christine Paulin-Mohring (Orsay), Frank Pfenning (Pittsburgh),
  Femke van Raamsdonk (Amsterdam), Mark-Oliver Stehr (Urbana), Rakesh Verma
  (Houston), Andrei Voronkov (Manchester).



SEVENTH INTERNATIONAL CONFERENCE ON TYPED LAMBDA CALCULI AND
APPLICATIONS (TLCA 05)
  Nara, Japan, 21-23 April 2005
  Colocated with RTA'05 as RDP 2005
  http://www.kurims.kyoto-u.ac.jp/rdp05/tlca/
  Call for Papers
* The TLCA series of conferences serves as a forum for presenting original
  research results that are broadly relevant to the theory and applications
  of typed lambda calculi and related systems.
* The programme of TLCA'05 will consist of three invited talks and about
  25 papers selected from original contributions. Accepted papers will
  be published as a volume of Springer Lecture Notes in Computer Science
  series.
* Deadlines:
  Titles and abstracts due:  October 25, 2004
  Paper submission deadline: November 2, 2004
* Invited Speakers: Thierry Coquand (Goteborg), Amy Felty (Ottawa),
  Susumu Hayashi (Kobe)
* For details see webpage



17TH INTERNATIONAL CONFERENCE ON COMPUTER AIDED VERIFICATION (CAV 2005)
  July 6-10, 2005, University of Edinburgh, Scotland, UK
  http://www.cav2005.inf.ed.ac.uk/
  Call For Papers
* CAV'05 conference is the 17th 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. The proceedings of
  the conference will be published in the Springer-Verlag Lecture Notes in
  Computer Science series.
* Paper submission (strict): January 21, 2005
* Kousha Etessami, University of Edinburgh kousha@inf.ed.ac.uk, Sriram
  Rajamani, Microsoft Research  sriram@microsoft.com
* For details see webpage



21ST BRITISH COLLOQUIUM FOR THEORETICAL COMPUTER SCIENCE (BCTCS 2005)
  Announcement
  22-24 March 2005, University of Nottingham, England
  http://www.cs.nott.ac.uk/~gmh/bctcs05.html
* Purpose.  The purpose of BCTCS is to provide a forum in which researchers
  in theoretical computer science can meet, present research findings, and
  discuss developments in the field. It also aims to provide an environment
  in which PhD students can gain experience in presenting their work, and
  benefit from contact with established researchers.
* Scope.  The scope of the colloquium includes all aspects of theoretical
  computer science, including algorithms, complexity, semantics, formal
  methods, concurrency, types, languages and logics. Both computer scientists
  and mathematicians are welcome to attend, as are non-UK participants.
* Programme. The programme will consist of two and a half days of invited
  talks, tutorials, and contributed talks.  Invited speakers: Alan Gibbons,
  King's College London (sponsored by the LMS); Andrew Gordon, Microsoft
  Research, Cambridge; Ralf Hinze, University of Bonn; Conor McBride,
  University of Durham; Rajeev Raman, University of Leicester.
* Registration and submission deadline: 7th February 2005.



LOGIC COLLOQUIUM '05 - A.S.L. EUROPEAN SUMMER MEETING
  Athens, Greece, July 28 - August 3, 2005
  http://www.math.uoa.gr/lc2005
  Call for Abstracts and Participation
* The conference is devoted to the following areas of Mathematical
  Logic: Computability Theory, Computer Science Logic, Model Theory,
  Philosophy of Logic, Proof Theory and Set Theory. The scientific
  program will consist of four short courses, twelve plenary lectures,
  four special sessions and presentations of contributed papers.
* Invited speakers include: P. Aczel (Univ. of Manchester, U.K.),
  I. Ben-Yaacov (Univ. of Wisconsin, Madison), J. Bergstra (Univ.
  of Amsterdam), S. Goncharov (Novosibirsk State Univ., Russia),
  D. Haskell (McMaster Univ., Canada), E. Jaligot (Univ. of
  Paris VII, France), Ph. G. Kolaitis (I.B.M. Almaden Research Center
  and U.C.S.C.), J. Moore (Boise State Univ., Idaho), C. Parsons
  (Harvard Univ.), H. Schwichtenberg (Univ. of Munich, Germany),
  M. Sheard (Saint Lawrence Univ., New York), S. Tupailo (Tallinn
  Univ. of Technology, Estonia), K. Weihrauch (Univ. of Hagen,
  Germany), J. Zapletal (Univ. of Florida, Gainesville).
* Abstracts of contributed talks should be submitted by April 15, 2005,
  to: Logic Colloquium 2005, Department of Mathematics, University of
  Athens, GR-157 84 Zografou, Greece (email: lc2005@math.uoa.gr).
* Program Committee: C. T. Chong (Univ. of Singapore), C. Dimitracopoulos
  (Univ. of Athens, Greece), G. Jaeger (Univ. of Bern, Switzerland),
  H. Field (New York Univ.), G. Metakides (Univ. of Patras, Greece),
  L. Newelski (Univ. of Wroclaw, Poland), D. Normann (Univ. of Oslo, Norway),
  R. Parikh (City Univ. of New York), J. Steel (University of California,
  Berkeley), S. Todorcevic (Univ. of Paris VII, France), J. Tucker
  (Univ. of Wales, Swansea), F. Wagner (Univ. of Lyon 1, France),
  S. Wainer (Univ. of Leeds, U.K., Chair).



VISSAS 2005
  Verification of Infinite State Systems with Application to Security
  March 17-22, 2005
  Timisoara, Romania
  http://vissas.ieat.ro/
  Call for Papers
* VISSAS 2005 is a NATO Advanced Research Workshop providing a
  forum to discuss research issues and address challenges in
  verification of infinite-state systems with applications to
  security.
* Deadline for paper submissions: November 1, 2004
* For details see webpage



COORDINATION 2005
  20-23 April 2005, Namur, Belgium
  Call for Papers
  http://www.coordination2005.org
* Modern information systems rely increasingly on combining concurrent,
  distributed, mobile, reconfigurable and heterogenous components. New
  models, architectures, languages, verification techniques are
  necessary to cope with the complexity induced by the demands of
  today's software development. Coordination languages have emerged as a
  successful approach, in that they provide abstractions that cleanly
  separate behavior from communication, therefore increasing modularity,
  simplifying reasoning, and ultimately enhancing software development.
* Building on the success of the previous editions, this conference
  provides a well-established forum for the growing community of
  researchers interested in models, languages, architectures, and
  implementation techniques for coordination.
* Submission of abstracts: December 15, 2004
  Submission of papers: December 21, 2004
* for details see webpage



6TH INTERNATIONAL CONFERENCE ON FORMAL ENGINEERING METHODS (ICFEM 2004)
  Nov 8-12, 2004, Seattle, USA
  http://research.microsoft.com/conferences/icfem2004/
  Call for Participation
* ICFEM 2004 aims to bring together those interested in the application
  of formal engineering methods to computer systems. Researchers and
  practitioners, from industry, academia, and government, are encouraged
  to attend, and to help advance the state of the art. We are interested
  in work that has been incorporated into real production systems, and
  in theoretical work that promises to bring practical, tangible benefit.
* ICFEM 2004 features one workshop five half-day tutorials, 4 invited
  talks, 30 technical papers in 9 sessions covering various aspects of
  formal engineering: formal specification, verfication, analysis,
  model checking.
* For details see website



JOURNAL OF AUTOMATED REASONING SPECIAL ISSUE
  Automated Reasoning for Security Protocol Analysis
  http://www.avispa-project.org/arspa
* Editors: Alessandro Armando (Genova), David Basin (ETH Zurich),
  Jorge Cuellar (Siemens AG, Munich), Michael Rusinowitch
  (LORIA-INRIA-Lorraine), Luca Vigano` (ETH Zurich)
* Neadline for submission: November 26 2004
* For more details see webpage



BOOK ANNOUNCEMENT
  Logic Colloquium '99; Lecture Notes in Logic 17
  Edited by Jan van Eijck, Vincent van Oostrom, Albert Visser
  Association for Symbolic Logic, 2004
  Paperback; ISBN 1-56881-203-5; US$40.00
  Hardcover; ISBN 1-56881-199-3; US$70.00
  http://www.akpeters.com
* A compilation of papers presented at the 1999 European Summer
  Meeting of the Association for Symbolic Logic, Logic
  Colloquium '99 includes surveys and research articles from some
  of the world's preeminent logicians. Two long articles are based
  on tutorials given at the meeting and present accessible
  expositions of current research in two active areas of logic,
  geometric model theory and descriptive set theory of group actions.
* The other articles cover current reseach topics in all areas
  of mathematical logic, including logic in computer science, proof
  theory, set theory, model theory, computability theory, and philosophy.
* Ordering information. See the URL above.



BOOK ANNOUNCEMENT
  Logic in Computer Science
  Second Edition
  by Michael Huth and Mark Ryan.
* A textbook that provides a sound basis in logic, and introduces logical
  frameworks used in modelling, specifying and verifying computer systems.
* Foreword; 1. Propositional logic; 2. Predicate logic; 3. Verification
  by model checking; 4. Program verification; 5. Modal logics and agents;
  6. Binary decision diagrams; Bibliography; Index.
* "This is an excellent textbook on logic and formal methods which is
  very suitable for computer science students."
  From review of first edition in Theory and Practice of Logic Programming
* For more information, please visit:
  http://www.cambridge.org/computerscience/huthryan



PHD OR POSTDOC POSITION AT HU BERLIN
* Applications are invited for a two or three year research position in
  Theoretical Computer Science at the Humboldt-University at Berlin. The
  position is within the research project
  "The complexity of constraint satisfaction problems"
  (http://www.informatik.hu-berlin.de/logik/forschung/csp-en.html).
* Candidates are required to a have a degree in Mathematics or Computer
  Science. Both post-doc and pre-doc applications are welcome; it will be
  possible to work towards a doctoral degree.  Excellent knowledge of
  Theoretical Computer Science and Mathematics is expected.
* Applications should be sent to the following address until
  30. November 2004:
      Prof. Dr. Martin Grohe
      Humboldt-Universitaet zu Berlin
      Institut fuer Informatik
      Unter den Linden 6
      10099 Berlin
      Germany
* Informal enquiries may be addressed to grohe_at_informatik.hu-berlin.de.



NOMINATIONS SOUGHT FOR NEVALINNA PRIZE
  Deadline for nominations is December 15, 2004,
* The Nevanlinna Prize recognizes outstanding contributions
  to mathematical aspects of information science, including:
  1. All mathematical aspects of computer science,
    including complexity theory, logic of programming
    languages, analysis of algorithms, cryptography,
    computer vision, pattern recognition, information processing,
    and modeling of intelligence;
  2. Scientific computing and numerical analysis. Computational
    aspects of optimization and control theory. Computer algebra.
* Details about eligibility and submission of nominations are at
  www.mathunion.org/General/Prizes/Nevanlinna/index.html
* Please note the age restriction: nominees must be strictly less
  than 40 on December 31, 2005.
* The prize will be awarded at the 2006 International Congress of
  Mathematicians.



Back to the LICS web page.