From the AAR President, Larry Wos... This first issue of the AAR Newsletter for 2006 includes calls for papers, presentations, and demonstrations at conferences worldwide. Of especial interest is FLoC, which combines six conferences and hosts over 40 workshops. I encourage our members to participate; this burgeoning interest in automated reasoning is most exciting and gratifying.

The Herbrand Award is given by CADE Inc. to honor a person or group for exceptional contributions to the field of Automated Deduction. At most one Herbrand Award will be given at each CADE or IJCAR meeting. The Herbrand Award has been given in the past to

Larry Wos (1992)

Woody Bledsoe (1994)

Alan Robinson (1996)

Wu Wen-Tsun (1997)

Gerard Huet (1998)

Robert S. Boyer and J Strother Moore (1999)

William W. McCune (2000)

Donald W. Loveland (2001)

Mark E. Stickel (2002)

Peter B. Andrews (2003)

Harald Ganzinger (2004)

Martin Davis (2005)

A nomination is required for consideration for the Herbrand award.
The deadline for nominations for the Herbrand Award that will be given at IJCAR 2006 is the

Nominations should consist of a letter (preferably email) of up to 2,000 words from the principal nominator, describing the nominee's contribution, along with letters of up to 2,000 words of endorsement from two other seconders. Nominations should be sent to

Call for Papers

LFMTP'06

The International Workshops on Logical Frameworks and Meta-Languages: Theory and Practice (affiliated with LICS and IJCAR at FLOC'06) will take place in Seattle, Washington, August 16, 2006.

The theme is the automation and implementation of the meta-theory of programming languages and related calculi, particularly work which involves variable binding and fresh name generation. Of interest are the theoretical and practical issues concerning the encoding of variable binding and fresh name generation, especially the representation of, and reasoning about, datatypes defined from binding signatures. Case studies of meta-programming are welcome, as is the mechanization of the (meta)theory of programming languages and calculi.

Paper submissions fall into three categories:

• Category A: Detailed and technical accounts of new research: up to 15 pages including bibliography.
• Category B: Shorter accounts of work in progress: up to 8 pages including bibliography.
• Category C: System descriptions, presenting an implemented tool and its novel features: up to 6 pages. A demonstration is expected to accompany the presentation.

For submission instructions, see the LFMTP Web site. The submission deadline is May 15, 2006.

FLoC'06

The 2006 Federated Logic Conference will take place in Seattle, Washington, August 10-22, 2006.

The following conferences will participate in FLoC'06:

• Int'l Conference on Computer-Aided Verification (CAV)
• Int'l Conference on Rewriting Techniques and Applications (RTA)
• IEEE Symposium on Logic in Computer Science (LICS)
• Int'l Conference on Logic Programming (ICLP)
• Int'l Conference on Theory and Applications of Satisfiability Testing (SAT)
• Int'l Joint Conference on Automated Reasoning (IJCAR)

Calls for papers for the conferences and workshops are available at the conference Web site. We invite you to submit papers to FLoC'06 conferences and workshops.

PDPAR 2006

The 4th International Workshop on Pragmatics of Decision Procedures in Automated Reasoning will be held in Seattle, Washington, August 21, 2006.

Decision procedures are key components within many formal verification and automated reasoning tools. Their performance, capacity, and scalability are vital to the tools that depend on them. Furthermore, new extensions may allow the formal verification or automated reasoning tools to use decision procedures more effectively. The goal of this workshop is to bring together researchers interested in making new decision procedures possible, and old decision procedures more powerful and more useful.

Topics of interest include new decision procedures, new methods of implementing decision procedures, new ways of using of the infrastructure common to decision procedures, and applications and case studies.

PDPAR will accept two types of papers:

• Original papers: should describe original research and contain sufficient detail to assess the merits and relevance of the contribution. Simultaneous submission of material is prohibited. Given the informal style of the workshop, the submission of papers presenting student's work and work in progress is encouraged.
• Presentation-only papers: describe work previously published in non-FLOC'06 forums, and will not be inserted in the proceedings. We are allowing the submission of previously published work in order to allow researchers to communicate good ideas that the PDPAR attendees are potentially unaware of.

Submissions should be sent by email to pdpar06@dit.unitn.it. Further information about how to submit papers will be made available at the Web site.

The authors of accepted submissions are expected to give a presentation at the workshop. They will be asked for the files of their presentations, which will be made available on the workshop's web page after the workshop.

LICS 2006

The twenty-first Annual IEEE Symposium on Logic in Computer Science (LICS 2006) will take place August 12-15, 2006, in Seattle, Washington. LICS 2006 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 2006 submission site between April 15 and April 21, 2006:

LCC'06

A workshop on Locig and Computational Complexity (affiliated with LICS 2006) will take place in Seattle, Washington, August 10-11, 2006. Topics of interest include complexity analysis for functional languages, complexity in database theory, complexity in formal methods, computational complexity in higher types, formal methods for complexity analysis of programs, foundations of implicit computational complexity, logical and machine-independent characterizations of complexity classes, logics closely related to complexity classes, proof complexity semantic approaches to complexity, software that applies LCC ideas, and type systems for controlling complexity.

The submission deadline is June 12, 2006. See the workshop Web site for details.

WRS06

The Sixth international Workshop on Reduction Strategies in Rewriting and Programming will take place in Seattle, Washington, August 11, 2006.

The workshop intends to promote and stimulate international research and collaboration in the area of evaluation strategies. It encourages the presentation of new directions, developments, and results as well as surveys and tutorials on existing knowledge in this area.

Reduction strategies study which subexpression(s) of an expression should be selected for evaluation and which rule(s) should be applied. These choices affect fundamental properties of a computation such as laziness, strictness, completeness, and need. . For this reason some programming languages (e.g., Elan, Maude, OBJ, and Stratego) allow the explicit definition of the evaluation strategy, whereas other languages (e.g., Clean, Curry, and Haskell) allow its modification. Strategies pose challenging theoretical problems and play an important role in practical tools such as theorem provers, model checkers, and programming languages.

Abstracts must be submitted by May 8, 2006; full papers are due May 15. Topics of interest include the following:

• theoretical foundations for the definition and semantic description of reduction strategies
• strategies in different frameworks such as term rewriting, graph rewriting, infinitary rewriting, lambda calculi, higher order rewriting, conditional rewriting, rewriting with built-ins, narrowing, and constraint solving
• application of strategies to equational, functional, functional-logic programming languages

• properties of reduction strategies and corresponding computations

• interrelations, combinations, and applications of reduction under different strategies

• program analysis and other semantics-based optimization techniques dealing with reduction strategies

• rewrite systems, tools, implementations with flexible or programmable strategies as an essential concept or ingredient

• specification of reduction strategies in real languages strategies suitable to software engineering problems and applications tutorials and systems related to evaluation strategies

For further information, see the Web page.

STRATEGIES 2006

The sixth international workshop on Strategies in Automated Deduction is a successor to both the series of STRATEGIES workshops associated with CADE and IJCAR and to the STRATA 2003 workshop associated with TPHOLs. Papers and participation are invited from both the fully automatic and interactive theorem proving communities.

For the full call for papers see the Web site.

AIML-2006

The ``Advances in Modal Logic" conference will take place September 25-28, 2006, in Noosa (Queensland, Australia).

Advances in Modal Logic is an initiative aimed at presenting an up-to-date picture of the state of the art in modal logic and its many applications. The initiative consists of a conference series together with volumes based on the conferences.

Submissions are invited on all aspects of modal logics, including the following:

• applications of modal logic
• computational aspects of modal logics
• history of modal logic
• philosophy of modal logic
• specific instances of modal logic
• theoretical aspects of modal logic
• variations of modal logic

For further information, see the Web site.