Community News

List of News:

Summer School on Constraint Programming
September 11-15, Acquafredda di Maratea, Italy



Since its origin in the mid 80's, Constraint Programming (CP) has become a widely used programming paradigm for solving constraint satisfaction and optimization problems. The distinguishing feature of CP is that it provides a clear distinction between the problem modelling and the algorithms and heuristics used to solve it.
The first international summer school on constraint programming is organised for PhD students, researchers, and practitioners interested in an extensive introduction to CP concepts such as problem modelling, constraint propagation, global constraints, and search.
Leading experts in the field will give invited tutorial lectures on different aspects of constraint programming along with practical exercises. Lecturers will evaluate the work of the students. This will provide the participants with a useful feedback.
Lecturers will evaluate the work of the students, so that Ph.D. students will be able to use the school to cover some of their coursework.


The program of the school will include the following courses:

Each lecturer will deliver four 1hr lectures, for a total of 24 hours throughout the school.

School site

The school will take place in hotel "Villa del Mare" in Acquafredda di Maratea, in the Basilicata region of Italy. The hotel is on the Tyrrenian sea, in an area where the mountains meet the sea, called the gulf of Policastro. Information on how to reach the school location will be posted on this site soon.


The early registration fee (by June 30) is 300 euros. The late registration fee (by July 31) is 350 euros. To register, please fill the registration form and fax it to the number indicated in the form, after having paid the registration fee by bank transfer by the due date. Some student grants might be available at a later stage. Information about these grants will be available on the school website.

Hotel reservation

The cost of a double room is 80 euros per day (per person), while a single room costs 90 euros per day. This cost includes all meals. To reserve your room at hotel Villa del Mare, please fill the accomodation form and fax it to the hotel before August 20.

Important dates


TYPES Summer School 2005
Proofs of Programs and Formalization of Mathematics
August 15-26, Goteborg, Sweden

Communicated by Bengt Nordstrom

During the last ten years major achievements have been made in using computers for interactive proof developments to produce secure software and to show interesting mathematical results. Recent major results are, for instance, the complete formalisation of a proof of the four colour theorem, and a formalisation of the prime number theorem. See the following articles in The Economist and Science:

The summer school is a two weeks' course for postgraduate students, researchers and industrials who want to learn about interactive proof development. The present school follows the format of previous TYPES summer school (in Baastad 1993, Giens 1999, Giens 2002).  There will be introductory and advanced lectures on lambda calculus, type theory, logical frameworks, program extraction, and other topics with relevant theoretical background.  Several talks will be devoted to applications.

During these two weeks we will present three proof assistants: Coq, Isabelle and Agda, which are state-of-the-art interactive theorem provers.  Participants will get extensive opportunities to use the systems for developing their own proofs. No previous knowledge of type theory and lambda calculus is required.

The school is organised by the TYPES working group "Types for Proofs and Programs", which is a project in the IST (Information Society Technologies) program of the European Union. A limited number of grants covering part of travel, fees and ackommodation are available. Neither participation nor grants are restricted to TYPES participants.


The organising committee: Andreas Abel, Ana Bove, Catarina Coquand, Thierry Coquand, Peter Dybjer and Bengt Nordstrom.

Summer School "Aspects of Complexity"
July 18-28, 2005, University of Bologna, Italy

Communicated by Guido Fioretti

The University of Bologna First Summer School on "Aspects of Complexity" offers an intensive 10-day introduction to the dynamics of complex systems in the computer, natural and social sciences. Examples of the complex systems that will be examined include computer networks (such as the internet), textual networks (such as those emerging from the co-occurrence of words contained in media reports), biological systems (such as ant colonies), markets (such as the stock exchange), business organizations, and social systems defined at various scales.
The program will stress the distributed nature of decision and communication processes that imply storage, processing and retrieval of information.

For further information and registration details, please consult

Summer School
Foundations of Security Analysis and Design
September 19-24, 2005, Bertinoro, Italy

Communicated by Roberto Gorrieri

General Information
Security in computer systems and networks is emerging as one of the most challenging research areas for the future. The main aim of the school is to offer a good spectrum of current research in foundations of security, ranging from programming languages to analysis of protocols, that can be of help for graduate students, young researchers from academia or industry that intend to approach the field.
The FOSAD series started in 2000 and last edition was in 2004. This year the school covers one week (from Monday 19 to Saturday 24, September 2005) and alternates monographic courses of 4/6 hours and short courses of 2/3 hours. We also encourage presentations given by those participants that intend to take advantage of the audience for discussing their current research in the area.

The school is organized at the University Residential Center of Bertinoro, situated in Bertinoro, a small village on a scenic hill with a wonderful panorama, in between Forli' and Cesena (about 50 miles south-east of Bologna, 15 miles to the Adriatic sea). The cheapest way to travel is by plane to Forli' airport (the secondary airport of Bologna), which is daily connected to London and Frankfurt AM through the low fares airline Ryanair.

Lecturers and Courses
Gilles Barthe (INRIA Sophia Antipolis, France), Formal Methods for Smartcard Security
David Basin (ETH Zurich, Switzerland), Model-driven Security
Elisa Bertino (Purdue University, USA), Privacy Preserving Database Systems
Herve Debar (France Telecom R&D, France), Intrusion Detection
Theo Dimitrakos (BT Security Research, UK), GRID/Virtual Organizations Security
Fabio Massacci (Trento University, Italy), Security and Trust Requirements Engineering
Mogens Nielsen (BRICS, Aarhus, Denmark), Formal Model of Trust
Gene Tsudik (University of California, Irvine, USA), Wireless Network Security

The scientific school directors are
The administrative director is
Andrea Bandini (University Residential Centre of Bertinoro)
The local organizer is
Elena Della Godenza (University Residential Centre of Bertinoro)
Notice and Dates
Prospective participants should apply through the web site by
May 31, 2005.
Notification of accepted applicants will be posted by
June 15, 2005.
Registration to the school is due by
July 15, 2005.
Accommodation and Registration fees
Accommodation fee is 350 Euro and covers costs for 6 nights (starting from Sunday 18 September, 2005) in double room, half board (breakfast and lunch, dinner of 18 September 2005 included, lunch of 24 September 2005 excluded).
Registration fee is 350 Euro and includes didactical material from the lectures and a LNCS volume of the tutorial series, published by Springer, collecting material presented in FOSAD 2004 and FOSAD 2005.

A limited amount of grants will be provided to cover part of the expenses. Please, include your request with the application.

Further Information
More detailed information available at URL

University of Bologna

Under the auspices of:

* IFIP WG 1.7

ACM Transactions on Computational Logic
Call for Nominations

Communicated by Marco Comini

Nominations, including self nominations, are invited for the next  Editor-in-Chief of the  ACM Transactions on Computational Logic (ToCL), see: The position is for a
three-year term, starting on August 1, 2005; it may be renewed for a  second term.

Candidates should be well-established researchers in areas related to computational logic, broadly conceived. They should also have broad experience as journal editors and conference program committee members. Nominations, including a current curriculum vitae and a brief statement of their vision for ToCL, should be sent by June 1, 2005 to Moshe Y. Vardi <>.

Final selection will be made by a Selection Committee, consisting of Moshe Y. Vardi (chair), Rice University, Joseph Y. Halpern, Cornell University, Gordon Plotkin, University of Edinburgh, and Wolfgang Thomas, RWTH Aachen.

Nominations received after June 1, 2005, will also be considered if the position is not yet filled.

Mathematical Structures in Computer Science
Special Issue on Theory and Application of Term Graph Rewriting

Communicated by Ian Mackie

Following from the success of the TERMGRAPH series of workshops, there will be a special issue of the journal Mathematical Structures in Computer Science (MSCS, Cambridge University Press), to be published in 2006, on Term Graph Rewriting. Submissions for this special issue are hereby solicited.

Term graph rewriting is concerned with the representation of expressions as graphs and their evaluation by rule-based graph transformation.  The advantage of using graphs rather than strings or
trees is that common subexpressions can be shared, which improves the efficiency of computations in space and time. Sharing is ubiquitous in implementations of programming languages: many implementations of functional, logic, object-oriented and concurrent calculi are based on term graphs. Term graphs are also used in symbolic computation systems and automated theorem proving. Research in term graph rewriting ranges from theoretical questions to practical implementation issues.

Topics for the special issue include: the modelling of first- and higher-order term rewriting by (acyclic or cyclic) graph rewriting, the use of graphical frameworks such as interaction nets and sharing graphs to model strategies of evaluation (for instance, optimal reduction in the lambda calculus), rewrite calculi on cyclic higher-order term graphs for the semantics and analysis of functional programs, graph reduction implementations of programming languages and automated reasoning, and symbolic computation systems working on shared structures.

Submissions should be sent electronically to Ian Mackie <> by 1st September 2005 (all submissions will be acknowledged). Information about the journal, including style files, can be found here:
Submissions will be refereed according to the usual very high standards of MSCS. Ian Mackie and Detlef Plump will serve as guest editors for this special issue. Final decisions on editorial matters rest with the editor-in-chief of MSCS.

Senior Research Fellowship
University of St. Andrews

Communicated by Ian Miguel

There is an outstanding opportunity to come to St Andrews to work with the constraints group here, which currently includes Ian Gent, Ian Miguel, Steve Linton, Tom Kelsey, and Colva Roney-Dougal.

The University of St Andrews is about to advertise two senior research fellowships for five years, where each has a non-competitive progression to permanant lecturer afterwards. One of these is expected to be in Computer Science and one in Mathematics, both to work on the new Multidisciplinary Critical Mass project funded by EPSRC in the Centre for Interdisciplinary Research in Computational Algebra.    More details are given below. Researchers with a constraint background will be in a strong position for  the CS job since some of the projects involve constraints research.

We hope that the combination of a 5 year research job in an exciting area, together with the non-competitive progression to a permanent lectureship, should be extremely attractive.

Please note at this stage we are looking for expressions of interest -- the formal advertisement requiring job applications will be published shortly.    Expressions of interest should be sent to Steve Linton, though of course you can also ask me any questions.
If you are not interested yourself, please feel free to pass this on to others you might know who would be interested, and/or to circulate it to your colleagues.

Ian Gent


Two Senior Research Fellowship in Computational Algebra
(with non-competitive progression to Lectureships)

Starting Salary: £27116 - £35883 pa (not including 2005 pay rise)

Advance announcement, formal advertisement will follow

The Centre for Interdisciplinary Research in Computational Algebra (CIRCA) expects shortly to advertise two vacancies for Senior Research Fellows (RA2 scale) in connection with the recently awarded grant "Multidisciplinary Critical Mass in Computational Algebra and Applications" (EPSRC EP/C523229).  The appointments will begin during the 2005/6 academic year and continue until the end of the grant in August 2010.  Subject to the successful outcome of a non-competitive review of their performance about two years after appointment, it is expected that one of the appointees will then progress to a lectureship in Pure Mathematics and one to a lectureship in Computer Science.

Details of this proposal can be found at; more information about CIRCA can be found at The two senior fellows will each be expected to contribute to several of the projects which make up this proposal, and also to take a role in project management and the development of new projects as described in the proposal.

The successful candidates should have the following qualities:
For  additional  information or  to  make  informal enquiries,  please contact  Steve  Linton,,  tel:  +44 1334  463269. Formal  advertisements  should appear  soon  on  the University's  job vacancies Web page, and in the press.

Bell Labs Ireland
PostDoc Position in Operations Research/Computer Science

Communicated by Ian Miguel

Bell Labs, the innovation engine of Lucent Technologies, is a worldwide research and development community that focuses its efforts on key technologies including Software, Wireless and Broadband networking, Signal Processing, Microelectronics, Photonics and Supply Chain technology. It is internationally renowned as the birthplace of modern information theory, the transistor, the laser and the UNIX operating system.

Bell Labs is recruiting for multiple positions within its new research facility in Dublin, Ireland. Well-funded, leading edge research will begin focusing on next generation fixed and wireless communications networks and other new emerging voice/ data technologies.

We are presently recruiting for a Post-Doctoral Contract Position (duration 2 years) in the areas of:
This unique position will afford the opportunity for strong collaborative research with researchers at the Cork Constraint Computation Centre (4C) at the University College Cork.

To be considered for this position, you must have a Ph.D. in computer science, operations research, mathematics, statistics, or related fields with extensive programming experience.  A comprehensive and competitive benefits package exists which would include relocation costs.

To receive role profiles and apply, Please contact Helen Creedon on +3531-886 4496. You will need to send an up-to-date CV (Including a full publications list) to and eohanlon@4c.ucc.i

PostDoc Position in Formal Methods and Techniques of Refinement

Communicated by Dominique Mery

The MOSEL project is supported by INRIA, CNRS and the three universities of Nancy. INRIA is making lots of post doc positions available for the next academic year. One of these is described below:

General information about dates, eligibility, etc.

Post doc description:



Application procedure:

Summary on the postdoc proposal:
Topics: Refinement-based design of software/hardware systems
Required skills: The applicant should be fluent in formal methods applied to embedded systems; he or she should master a formal method and a theorem prover.
Supervisor: Dominique Méry at LORIA

Summer School on Logic-based Knowledge Representation
Technische Universitat Dresden, July 2-17, 2005

Communicated by Alex Simpson

As in the summer schools at TU Dresden in 2002, 2003, and 2004, people from distinct, but communicating communities will gather in an informal and friendly atmosphere. This two-week event is aimed at graduate students and researchers.


The topic of this year´s summer school is: Logic-based Knowledge Representation.

Intelligent behavior is hard to imagine without the agent having a good knowledge about the surrounding world. For this reason, knowledge representation always played a crucial role in artificial intelligence. Right from the beginning of the field, there was a big discussion on whether sub-symbolic or symbolic approaches for representing knowledge are the right way to go. And even within the symbolic approach there was a conflict between proponents of logic-based approaches (like John McCarthy and Pat Hayes) and proponents of graph-based or procedural approaches (like Marvin Minsky).

The advantage of logic-based approaches for symbolic knowledge representation is that they provide the representation formalism with a formally well-founded semantics, which makes both the represented knowledge and the behavior of knowledge representation systems deducing implicit knowledge from the explicitly represented one comprehensible. The disadvantage is that the inference problems may become intractable or even undecidable if the expressive power of the formalism is large enough. For this reason, early systems employing the logic-based approach were either too inexpressive or too slow.

This situation has changed drastically in the last 10-15 years. This is partially due to increased computing power. More importantly, however, were the recent theoretical and practical advances in the field of logic-based knowledge representation. The summer school will focus on several of the most successful subfields of this active research area:

Please consult the Course Program for further details.


If you want to attend the summer school, we would like you to register via the Online Registration Form.
For all who wanted to apply for a grant, 9th April 2005 was the obligatory registration deadline. Now registration is possible as long as there are vacant places. (Since we intend to restrict participation to about 60 people, in case of excessive demand, we will have to select applicants to the summer school.)
Persons who applied until 9th April will be informed about admittance and decisions on grants until 18th April 2005.


We ask for a participation fee of 200 EUR. Please pay this summer school fee cash at the day of your arrival.

Integrated workshop

It will be possible for some participants to present their research work during a small workshop integrated in the summer school. Please indicate in the registration form if you would like to do so. You are asked to submit an extended abstract consisting of no more than 5 pages. The deadline to register for the workshop is 9th April 2005.
A program committee consisting of the summer school lecturers and organizers will select among the proposals. Notification of acceptance of a talk at the integrated workshop will be by 10th May 2005.


A limited number of grants may be available, please indicate in your application if the only possibility for you to participate is via a grant. Applications for grants must include an estimate of travel costs and they should be sent together with the registration.


We will provide assistance in finding an accommodation in Dresden.


Communicated by Roberto Bagnara

I am very happy to announce the availability of CLAIR 1.0. CLAIR is a system that has been developed in order to study and experiment with various aspects of the definition and implementation of programming languages.  In particular it is aimed at providing easy ways of playing with:
  1. lexical analysis;
  2. syntactic analysis and generation of the abstract syntax tree;
  3. static checking of type correctness;
  4. operational semantics expressed by means of transition systems;
  5. interpretation;
  6. static analysis;
  7. compilation.
While points 1-5 are fully developed, points 6 and 7 do not exist yet.  At present, CLAIR supports two languages: a simple functional language (SFL) and an imperative language (SIL) that recalls Pascal to some extent.  Both languages adopt the static scoping rule.

The CLAIR approach is based on structured operational semantics a` la Plotkin for the formal description and on the Prolog language for the implementation.  One of the advantages of this combined approach is that it is relatively easy to extend the system so as to support other language features.  CLAIR is currently being used successfully in university courses covering formal languages and operational semantics.  Its main advantage is that students can see, with relatively little effort, theory at work: a grammar becomes a parser, static semantics rules directly translate into a type checker, and with dynamic semantics rules you have an interpreter for your language (students are deeply impressed when they see the interpreter actually running the imperative programs).  We hope to add facilities that allow to easily turn an abstract semantics into a static analyzer.

Compilation of the system is as easy as typing `./configure' and `make', provided at least one of the following Prolog systems is available:
CLAIR is distributed under the terms of the GNU General Public License. Feedback is solicited on all aspects of the system and its documentation.
For more information, visit the CLAIR web site at

The Constraint Handling Rules Web-Pages

Communicated by Thom Fruehwirth

The Constraint Handling Rules (CHR) web-pages have been moved and updated:

CoLoR, a Coq Library on Rewriting and Termination

Communicated by Frederic Blanqui

I am pleased to announce the release of the first version of CoLoR, a Coq Library on Rewriting and termination. Coq is a proof assistant developped at INRIA available at The aim of this Coq library is to provide the necessary formal basis for certifying the termination witnesses searched and built by termination tools like CiME, AProVE, TTT, Cariboo, etc.

For the moment, among other things, it includes:
The library is likely to evolve and include more developments quickly. Contributions on RPO and HORPO are on the way, with a library on finite multisets. If you are interested, you can join our working group. Contributions to this project are very welcome!

For announcements and discussions, you can subscribe to the CoLoR mailing list

You can download the library and get more information on the CoLoR web page The library is distributed under the terms of the french free software license CeCILL, that is compatible with the GNU General Public License.

Formal Methods Letter (FML)

Communicated by Susanne Graf

Dear colleagues,

We would like to cordially invite you to submit a paper to Formal Methods Letters (FML), a new publication whose goal is to address the need in the formal methods community for a publication outlet with a rapid turn-around time for short papers.

FML will publish papers of just a few pages describing recent research advances, as a quarterly special section of the journal Software Tools for Technology Transfer. FML papers will be electronically available as soon as they are ready for publication, and freely accessible to all. They will subsequently appear in the paper version of the journal. Thus, space limitations in the paper journal will not be a barrier to rapid publication.

FML is intended to provide a channel for fast publication of new and original ideas. It will provide a venue for quickly disseminating theoretical and experimental results, and also a means of publishing new approaches that are sound and of interest to the community, but may not yet be fully supported by implementation and experiment. In addition, it will offer a chance to publish new work without traveling great distances to deliver it.

Unlike other venues for short papers, FML will be targeted solely at the formal methods community. By targeting a specific audience, we hope to build a regular readership that will check the website frequently for newly accepted papers.

Topics of interest for FML include but are not limited to:
In addition to research articles, FML welcomes short case studies and reports on practical or industrial application, as well as short resumes of new projects and tools that may be of interest to the community.

More information on FML, including information on electronic submissions can be found at
If you have any questions about the journal's policies or procedures, please feel free to contact the editors.

FML is intended as a resource for the formal methods community, allowing the rapid exchange of ideas via electronic media, while at the same time establishing priority for authors in an archived journal. If you have new ideas or results that could benefit from rapid dissemination, we hope that you will consider publishing them in FML.

        Best regards,

        Ken McMillan and Lenore Zuck
        Editors in chief

Advanced Topics in Types and Programming Languages
Book Announcement

Communicated by Benjamin Pierce

I am delighted to announce the availability of a new book:
Advanced Topics in Types and Programming Languages
Edited by Benjamin C. Pierce
MIT Press, 2005
ISBN 0-262-16228-8
  To order direct from Amazon...
For more information...

The study of type systems for programming languages now touches many areas of computer science, from language design and implementation to software engineering, network security, databases, and analysis of concurrent and distributed systems. This book offers accessible introductions to key ideas in the field, with contributions by experts on each topic.

The topics covered include precise type analyses, which extend simple type systems to give them a better grip on the run time behavior of systems; type systems for low-level languages; applications of types to reasoning about computer programs; type theory as a framework for the design of sophisticated module systems; and advanced techniques in ML-style type inference.

Advanced Topics in Types and Programming Languages builds on Benjamin Pierce's Types and Programming Languages (MIT Press, 2002); most of the chapters should be accessible to readers familiar with basic notations and techniques of operational semantics and type systems =D1 the material covered in the first half of the earlier book.

Advanced Topics in Types and Programming Languages can be used in the classroom and as a resource for professionals. Most chapters include exercises, ranging in difficulty from quick comprehension checks to challenging extensions, many with solutions.

I. Precise Type Analyses

Substructural Type Systems
by David Walker

Dependent Types
by David Aspinall and Martin Hofmann

Effect Types and Region-Based Memory Management
by Fritz Henglein, Henning Makholm, and Henning Niss

II. Types for Low-Level Languages

Typed Assembly Language
by Greg Morrisett

Proof-Carrying Code
by George Necula

III. Types and Reasoning about Programs

Logical Relations and a Case Study in Equivalence Checking
by Karl Crary

Typed Operational Reasoning
by Andrew Pitts

IV. Types for Programming in the Large

Design Considerations for ML-Style Module Systems
by Robert Harper and Benjamin C. Pierce

Type Definitions
by Christopher A. Stone

V. Type Inference

The Essence of ML Type Inference
by Francois Pottier and Didier Remy

An expanded table of contents and the book's preface are available from:

Logtalk 2.23.0 Released

Communicated by Paulo Moura

Logtalk 2.23.0 is now available for downloading from the Logtalk web site:

This release provides a significant performance improvement for applications which use an object's dynamic database, some bug fixes, and usability improvements. In addition, it contains all improvements since the previous major release (2.22.0). These includes updated support for several Prolog compilers (K-Prolog, XSB, and JIProlog), updated installation and documentation processing scripts, improved documentation and installation instructions, several performance improvements, and improved compiler error checking.