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:
will deliver four 1hr lectures, for a total of 24 hours throughout the
- Constraint propagation and backtracking-based search
(Rina Dechter, UC Irvine, USA)
- Scheduling tools and applications
(Claude Le Pape, Bouygues Telecom, France)
- Global constraints
(Jean-Charles Regin, ILOG, France)
- Soft constraints and over-constrained problems
(Thomas Schiex, INRA, France)
(Barbara Smith, 4C, Ireland)
- Hybrid algorithms, local search, and Eclipse
(Mark Wallace, Monash University, Australia)
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.
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
and fax it to the hotel before August 20.
- Early registration: before June 30, 2005
- Late registration: between July 1 and July 31, 2005
- Hotel reservation: before August 20, 2005
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:
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
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
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.
Bertot, INRIA Sophia
Miquel, Paris 7
Nipkow, TU Munich
Dowek, INRIA Futurs
Paulin, Paris Sud
Thery, INRIA Sophia
committee: Andreas Abel, Ana Bove, Catarina Coquand,
Thierry Coquand, Peter Dybjer and Bengt Nordstrom.
to Type Theory:
Inductive sets and families of sets
Predicative and non-predicative theories
applications and tools:
Proving properties of Java programs
Reasoning about Programming Languages
Correctness of floating-point algorithms
Dependently typed datastructures
Compiling dependent types
Fundamental theorem of algebra
Bishop' set theory
Other examples, e.g. prime number theorem
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
Foundations of Security Analysis and Design
September 19-24, 2005, Bertinoro, Italy
Communicated by Roberto Gorrieri
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
(ETH Zurich, Switzerland), Model-driven
(Purdue University, USA), Privacy Preserving
(France Telecom R&D, France), Intrusion Detection
(BT Security Research, UK), GRID/Virtual
(Trento University, Italy), Security and Trust
(BRICS, Aarhus, Denmark), Formal Model of
(University of California, Irvine, USA), Wireless Network
The scientific school directors are
Aldini (University "Carlo Bo", Urbino)
Gorrieri (University of Bologna)
Martinelli (CNR-IIT, Pisa)
The administrative director is
(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.
More detailed information available at URL
Under the auspices of:
* EATCS - IT
* ERCIM STM WG
* IFIP WG 1.7
ACM Transactions on Computational Logic
Call for Nominations
Communicated by Marco Comini
including self nominations, are invited for the next
of the ACM Transactions on Computational Logic (ToCL), see: http://www.acm.org/pubs/tocl/. The position is
term, starting on August 1, 2005; it may be renewed for a
should be well-established researchers in areas related to computational
logic, broadly conceived. They should also have broad
as journal editors and conference program committee members.
including a current curriculum vitae and a brief statement
vision for ToCL, should be sent by June 1, 2005 to
will be made by a Selection Committee, consisting of
Vardi (chair), Rice University, Joseph Y. Halpern, Cornell
Gordon Plotkin, University of Edinburgh, and Wolfgang
received after June 1, 2005, will also be considered if
position is not yet filled.
Mathematical Structures in Computer Science
Special Issue on Theory and Application of Term Graph Rewriting
Communicated by Ian Mackie
the success of the TERMGRAPH series of workshops, there will be a special
issue of the journal Mathematical Structures in
Science (MSCS, Cambridge University Press), to be published
on Term Graph Rewriting. Submissions for this special issue
rewriting is concerned with the representation of
as graphs and their evaluation by rule-based graph
The advantage of using graphs rather than strings or
trees is that
common subexpressions can be shared, which improves the
of computations in space and time. Sharing is ubiquitous in
of programming languages: many implementations of
logic, object-oriented and concurrent calculi are based on
graphs. Term graphs are also used in symbolic computation systems
automated theorem proving. Research in term graph rewriting ranges
theoretical questions to practical implementation issues.
Topics for the
special issue include: the modelling of first- and
term rewriting by (acyclic or cyclic) graph rewriting,
of graphical frameworks such as interaction nets and sharing
to model strategies of evaluation (for instance, optimal
in the lambda calculus), rewrite calculi on cyclic
term graphs for the semantics and analysis of functional
graph reduction implementations of programming languages and
reasoning, and symbolic computation systems working on
should be sent electronically to Ian Mackie
<email@example.com> by 1st September
2005 (all submissions will be
Information about the journal, including style files,
will be refereed according to the usual very high
of MSCS. Ian Mackie and Detlef Plump will serve as guest
for this special issue. Final decisions on editorial matters
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
here, which currently includes Ian Gent, Ian Miguel, Steve Linton, Tom
of St Andrews is about to advertise two senior research fellowships for
years, where each has a non-competitive progression to permanant
these is expected to be in Computer Science and one in Mathematics,
both to work on
Multidisciplinary Critical Mass project funded by EPSRC in the Centre
Research in Computational Algebra. More details are
with a constraint background will be in a strong position for the
some of the projects involve constraints research.
We hope that
the combination of a 5 year research job in an exciting area, together
non-competitive progression to a permanent lectureship, should be
Please note at
this stage we are looking for expressions of interest -- the formal
requiring job applications will be published shortly.
should be sent to Steve Linton, though of course you can also ask me
If you are not
interested yourself, please feel free to pass this on to others you
would be interested, and/or to circulate it to your colleagues.
Senior Research Fellowship in Computational Algebra
non-competitive progression to Lectureships)
£27116 - £35883 pa (not including 2005 pay rise)
announcement, formal advertisement will follow
The Centre for
Interdisciplinary Research in Computational Algebra
expects shortly to advertise two vacancies for Senior Research
(RA2 scale) in connection with the recently awarded grant
Critical Mass in Computational Algebra and
(EPSRC EP/C523229). The appointments will begin during
2005/6 academic year and continue until the end of the grant in
2010. Subject to the successful outcome of a non-competitive
of their performance about two years after appointment, it is
that one of the appointees will then progress to a
in Pure Mathematics and one to a lectureship in Computer
Details of this
proposal can be found at
http://www.dcs.st-and.ac.uk/~sal/MCM/; more information
found at http://www-circa.mcs.st-and.ac.uk/. The two senior
will each be expected to contribute to several of the projects
make up this proposal, and also to take a role in project
and the development of new projects as described in the
candidates should have the following qualities:
- A PhD or
equivalent qualifications or experience in an appropriate
of algebra and/or theoretical computer science, preferably some
research experience, and a track record of publications
potential to teach undergraduates in pure mathematics
computer science, preferably some teaching experience
programming experience, preferably including work in
algebra, and specifically work in GAP
and interests sufficient to contribute to at least two of
projects within the Multidisciplinary Critical Mass grant (in
the two appointments, we will be seeking complementary
to multidisciplinary research, in particular to
and promoting applications of computational algebra in
Science, Physics, Mathematics and elsewhere
communication, organisational, management and leadership
additional information or to make informal
Steve Linton, firstname.lastname@example.org, tel:
+44 1334 463269.
advertisements should appear soon on the
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
and development community that focuses its efforts on key
including Software, Wireless and Broadband networking,
Processing, Microelectronics, Photonics and Supply Chain
It is internationally renowned as the birthplace of modern
theory, the transistor, the laser and the UNIX operating system.
Bell Labs is
recruiting for multiple positions within its new research
in Dublin, Ireland. Well-funded, leading edge research will
focusing on next generation fixed and wireless communications
and other new emerging voice/ data technologies.
presently recruiting for a Post-Doctoral Contract Position
2 years) in the areas of:
position will afford the opportunity for strong
research with researchers at the Cork Constraint
Centre (4C) at the University College Cork.
considered for this position, you must have a Ph.D. in computer
operations research, mathematics, statistics, or related fields
extensive programming experience. A comprehensive and competitive
package exists which would include relocation costs.
To receive role
profiles and apply, Please contact Helen Creedon on
4496. You will need to send an up-to-date CV (Including a full
list) to email@example.com and firstname.lastname@example.org
PostDoc Position in Formal Methods and Techniques of Refinement
Communicated by Dominique Mery
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
General information about dates,
Post doc description:
on the postdoc proposal:
Refinement-based design of software/hardware systems
skills: The applicant should be fluent in formal methods applied to
systems; he or she should master a formal method and a theorem prover.
Dominique Méry at LORIA
Summer School on Logic-based Knowledge
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
The topic of this year´s summer school is: Logic-based Knowledge
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.
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:
the Course Program for further
- reasoning about action and change,
- nonmonotonic reasoning,
- description logics and ontologies, and
- action planning.
If you want to attend the summer school, we would like you to register
via the Online
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.
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
Communicated by Roberto Bagnara
I am very happy
to announce the availability of CLAIR 1.0.
a system that has been developed in order to study and
with various aspects of the definition and implementation
programming languages. In particular it is aimed at providing
1-5 are fully developed, points 6 and 7 do not exist
At present, CLAIR supports two languages: a simple functional
(SFL) and an imperative language (SIL) that recalls Pascal to
extent. Both languages adopt the static scoping rule.
analysis and generation of the abstract syntax tree;
checking of type correctness;
semantics expressed by means of transition systems;
approach is based on structured operational semantics a` la
for the formal description and on the Prolog language for the
One of the advantages of this combined approach is
is relatively easy to extend the system so as to support other
features. CLAIR is currently being used successfully in
courses covering formal languages and operational
Its main advantage is that students can see, with
little effort, theory at work: a grammar becomes a parser,
semantics rules directly translate into a type checker, and
dynamic semantics rules you have an interpreter for your language
are deeply impressed when they see the interpreter actually
the imperative programs). We hope to add facilities that
easily turn an abstract semantics into a static analyzer.
the system is as easy as typing `./configure' and
provided at least one of the following Prolog systems is
distributed under the terms of the GNU General Public License.
is solicited on all aspects of the system and its documentation.
information, visit the CLAIR web site at
The Constraint Handling Rules Web-Pages
Communicated by Thom Fruehwirth
Handling Rules (CHR) web-pages have been moved and updated:
CoLoR, a Coq Library on Rewriting and
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 http://coq.inria.fr/. 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!
- a library
- a library
on integer polynomials with multiple variables
- a library
on algebraic terms with symbols of fixed arity
- a proof
of the termination criterion based on polynomial interpretations
- a proof
of the dependancy pairs theorem
announcements and discussions, you can subscribe to the CoLoR mailing
download the library and get more information on the CoLoR web page http://www.loria.fr/~blanqui/color.html. 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
We would like
to cordially invite you to submit a paper to Formal
Letters (FML), a new publication whose goal is to address the
the formal methods community for a publication outlet with a
turn-around time for short papers.
publish papers of just a few pages describing recent research
as a quarterly special section of the journal Software Tools
Technology Transfer. FML papers will be electronically available
as they are ready for publication, and freely accessible to
They will subsequently appear in the paper version of the
Thus, space limitations in the paper journal will not be a
to rapid publication.
FML is intended
to provide a channel for fast publication of new and
ideas. It will provide a venue for quickly disseminating
and experimental results, and also a means of publishing
approaches that are sound and of interest to the community, but
yet be fully supported by implementation and experiment. In
it will offer a chance to publish new work without traveling
distances to deliver it.
venues for short papers, FML will be targeted solely at
formal methods community. By targeting a specific audience, we
build a regular readership that will check the website
for newly accepted papers.
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
of new projects and tools that may be of interest to the
Run-Time and Compiler Verification
Static Analysis Techniques
Compositional and Refinement-Based Methodologies
information on FML, including information on electronic
can be found at
If you have any
questions about the journal's policies or procedures,
feel free to contact the editors.
FML is intended
as a resource for the formal methods community,
the rapid exchange of ideas via electronic media, while at
time establishing priority for authors in an archived
If you have new ideas or results that could benefit from
dissemination, we hope that you will consider publishing them in
Ken McMillan and Lenore
Editors in chief
Advanced Topics in Types and Programming
Communicated by Benjamin Pierce
I am delighted to announce the availability of a new book:
Advanced Topics in Types and
Edited by Benjamin C. Pierce
MIT Press, 2005
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.
TABLE OF CONTENTS:
I. Precise Type Analyses
Substructural Type Systems
by David Walker
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
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
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
is now available for downloading from the Logtalk web site:
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.