NEWSLETTER No. 75, May 2007

From the AAR President
Herbrand Award
Kurt Gödel Centenary Research Prize Fellowships
Call for Papers

  • FTP07 -- New Category, New List of Speakers, New Deadline!
  • Logical and Semantic Frameworks, with Applications
  • LPAR 2007
  • Workshop on Visual Languages and Logic
  • ACM Workshop on Formal Methods in Security Engineering
  • ASCM 2007
  • School on Rewriting
    TABLEAUX 2007

    From the AAR President, Larry Wos...

    This issue of the AAR Newsletter is full of prizes! Alan Bundy has won the Herbrand Award, and outstanding candidates are invited to apply for five Kurt Gödel Centenary Research Prize Fellowships. I am especially pleased that the fellowships are to be awarded on the predoctoral and postdoctoral levels as well as the senior level: I believe it imperative to encourage new researchers in the field, as well as to reward those who have made outstanding contributions for many years. I am also excited about the continuing range of areas in which automated reasoning is being applied. Even within this small newsletter are announcements for conferences in security, visual languages and logic, rewriting, and mathematics.

    Herbrand Award

    It is my distinct honor to announce on behalf of the Board of Trustees of CADE Inc. that Alan Bundy is to receive the 2007 Herbrand Award for Distinguished Contributions to Automated Reasoning in recognition of his outstanding contributions to proof planning and inductive theorem proving, as well as to many other areas of automated reasoning and artificial intelligence.

    Franz Baader
    President of CADE Inc.

    Kurt Gödel Centenary Research Prize Fellowships

    The Kurt Gödel Society is proud to announce the commencement of the research fellowship prize program in honor of the celebration of Kurt Gödel's 100th birthday.

    The research fellowship prize program is sponsored by the John Templeton Foundation and will offer the following, based on an international open competition:

    Topics include model theory, proof theory, recursion theory, set theory, foundations of mathematics, founcations of computer science (related to logic), automated reasoning (related to logic), complexity (related to logic).

    The submission deadline is June 30, 2007. The fellowships begin March-Sept. 2008. Each proposal will be judged on the relevance of the research to the insights of Gödel, its general interest and clarity of motivation, and its reigorous scientific quality and depth.

    For further information, see the Web site or send email to

    Call for Papers

    FTP07 -- New Category, New List of Speakers, New Deadline!

    The Sixth International Workshop on First-Order Theorem Proving will take place at the University of Liverpool, UK, on September 12-13, 2007, co-locating with the Sixth International Symposium on Frontiers of Combining Systems on September 10-12, 2007.

    New Features. The workshop call for paper was announced in the January 2007 issue of the AAR Newsletter. In addition to the information presented there, we call your attention to the following new items.

  • Presentation-only Papers. These papers describe work recently published or submitted (no page limit). These will not be included in the proceedings, but preprints or postprints can be made available to participants. We see this as a way to provide additional access to important developments that FTP Workshop attendees may be unaware of.
  • Invited Speakers. Martin Giese (Linz, Austria); Bernd Fischer (Southampton, England, UK); Viorica-Sofronie Stokkermans, (Saarbruecken, Germany) [joint with FroCos]
  • Important Dates
    Paper submission deadline (all categories): June 29, 2007
    Notification of acceptance/rejection: July 23, 2007
    Final version due: August 3, 2007
    Workshop: September 12-13, 2007
  • For regular updates about the workshop organization, please see the FTP'07 Web page. To contact the program committee chair, please send an email to Silvio.Ranise[AT] (substitute [AT] with "@").


    The Second Workshop on Logical and Semantic Frameworks, with Applications will take place August 28, 2007, in Ouro Preto, Brazil. The objective of this one-day workshop is to bring together theoreticians and practitioners to promote new techniques and results, from the theoretical side, and feedback on the implementation and use of such techniques and results, from the practical side. Topics of interest to this forum include the following:

  • Logical frameworks
  • Proof theory
  • Type theory
  • Automated deduction
  • Semantic frameworks
  • Specification languages and meta-languages
  • Formal semantics of languages and systems
  • Computational and logical properties of semantic frameworks
  • Implementation of logical and/or semantic frameworks
  • Applications of logical and/or semantic frameworks
  • Papers must be submitted by May 19, 2007, with a maximum page count of 16 pages. The workshop pre-proceedings, containing the reviewed extended abstracts, will be handed-out at workshop registration and the proceedings will be published as a volume of ENTCS. For further information, see the Web page.

    LPAR 2007

    The 14th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2007) will be held October 15-19, 2007, in Yerevan, Armenia. Submission of papers for presentation at the conference is now invited. Topics of interest include the following:

    automated reasoning propositional reasoning
    interactive theorem proving description logics
    software verification hardware verification
    software testing logic and ontologies
    proof assistants network and protocol verification
    proof planning nonmonotonic reasoning
    proof checking constructive logic and type theory
    rewriting and unification lambda and combinatory calculi
    logic programming knowledge representation and reasoning
    modal and temporal logics constraint programming
    systems specification and synthesis logical foundations of programming
    model checking computational interpretations of logic
    proof-carrying code logic and computational complexity
    logic and databases logic in artificial intelligence
    reasoning for the semantic Web reasoning about actions

    Full and short papers are welcome. Full papers may be either regular papers containing new results or experimental papers describing implementations or evaluations of systems. Short papers may describe work in progress or provide system descriptions.

    Full-paper abstracts are due June 4; the full papers are due June 11. Dates for submission of short papers are to be arranged.

    The full-paper proceedings of LPAR 2007 will be published by Springer-Verlag in the LNAI series. The short-paper proceedings of LPAR 2007 will be published by the conference.

    For further information, see the Web site.

    Workshop on Visual Languages and Logic

    A Workshop on Visual Languages and Logic (VLL) will take place in Coeur d'Alene, Idaho, September 23, 2007.

    Original research papers are solicited that examine some combination of visual tools, representations or languages with logic. Topics of interest include the following:

    Submissions are due June 25, 2007, and should be no more than 12 pages. Authors of top-ranked papers will be invited to submit expanded versions for journal publication.

    Please see the Web site or email for further information.

    ACM Workshop on Formal Methods in Security Engineering

    The 5th ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code, will be held November 2, 2007, at George Mason University in conjunction with the ACM CCS'07.

    Information security has become a crucial concern for the commercial deployment of almost all applications and middleware. Although this is commonly recognized, the incorporation of security requirements in the software development process is not yet well understood. The deployment of security mechanisms is often ad hoc, without a formal security specification or analysis, and practically always without a formal security validation of the final product. Progress is being made, but there remains a wide gap between high-level security models and actual code development.

    This workshop aims to bring together researchers and practitioners from both the security and the software engineering communities, from academia and industry, who are working on applying formal methods to the design and validation of large-scale systems.

    Researchers are invited to submit original research papers addressing foundational issues in formal methods in security engineering in the following areas:

    Authors of accepted papers must guarantee that their paper will be presented at the workshop. Final proceedings will be published by the ACM.

    Submissions must be received by June 10, 2007. For submitting a paper, follow the guidelines on the FMSE'07 Web page.

    ASCM 2007

    The Eighth Asian Symposium on Computer Mathematics (ASCM 2007) will be held at the National University of Singapore, Singapore, Dec. 15-17, 2007.

    Research papers on all aspects of the interaction between computers and mathematics are solicited for the symposium. Specific topics include the following:

    Papers should be written in English, not exceeding 15 pages. Submission instructions are on the conference Web page. Papers are due August 31, 2007.

    A presymposium proceedings will be available at the conference in electronic form. A postsymposium proceedings is planned. The selected papers will be published as a volume in the Springer LNCS/LNAI series after the conference.

    School on Rewriting

    The Second International School on Rewriting (ISR'2007) will be held at LORIA, Nancy, France, July 2-6, 2007, just after the Federated Conference on Rewriting, Deduction, and Programming (RDP'07) held in Paris.

    This school is organized for master's and Ph.D. students, researchers, and practitioners interested in the study of rewriting concepts and applications. ISR is supported by the IFIP Working Group on Term Rewriting. The lectures will be given by experts on rewriting (termination, higher-order systems, strategies) and applications (security, theorem proving, program analysis and proofs).

    For more information see the Web site, or contact the organizers by e-mail: isr2007(at)loria(dot)fr

    TABLEAUX 2007

    TABLEAUX 2007 will take place in Aix en Provence, France, July 3-6, 2007. The conference brings together researchers interested in all aspects -- theoretical foundations, implementation techniques, systems development and applications -- of the mechanization of reasoning with tableaux and related methods. The conference will feature three invited speakers: Piero Bonatti, Università di Napoli; John-Jules Meyer, Utrecht University; and Cesare Tinelli, University of Iowa. Three tutorials also will take place: The Tableau Work Bench: Theory and Practice (P. Abate, R. Goré), fableau Methods for Interval Temporal Logics (V. Goranko, A. Montanari), and Semistructured Databases and Modal Logic (S. Cerrito). On-line registration is now open. Please note also the collocated workshop "Agents, Logic and Theorem Proving," July 3, 2007.

    Gail Pieper
    May 2007