• Summer School on Constraint Programming
  
• TYPES Summer School
  
• Summer School on Aspects of Complexity
  
• International School on Foundations of Security Analysis and Design
  
• ACM TOCL Call for Nominations
  
• MSCS Special Issue on Term Graph Rewriting
  
• Senior Research Fellowship, St. Andrews
  
• Bell Labs Ireland, PostDoc Position in Operation Research
  
• PostDoc Position in Formal Methods
  
• Summer School on Logic-based Knowledge Representation
  
• CLAIR 1.0
  
• Constraint Handling Rules Web-Pages
• CoLoR, a Coq Library on Rewriting and Termination
• Formal Methods Letter (FML)
• Book Announcement: Advanced Topics in Types and Programming Languages
• Logtalk 2.23.0 Released
  

Overview

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.

Program

The program of the school will include the following courses:

• 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)
• Modelling
  (Barbara Smith, 4C, Ireland)
• Hybrid algorithms, local search, and Eclipse
  (Mark Wallace, Monash University, Australia)

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.

Registration

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

• Early registration: before June 30, 2005
• Late registration: between July 1 and July 31, 2005
• Hotel reservation: before August 20, 2005

• Krzysztof R. Apt, National University of Singapore
• Michela Milano, University of Bologna, Italy
• Francesca Rossi, University of Padova, Italy

• Jeremy Avigad, Carnegie-Mellon    
• Connor McBride, Nottingham
• Yves Bertot, INRIA Sophia      
• Alexandre Miquel, Paris 7
• Thierry Coquand, Chalmers      
• Tobias Nipkow, TU Munich
• Catarina Coquand, Chalmers      
• Bengt Nordstrom, Chalmers
• Gilles Dowek, INRIA Futurs      
• Erik Palmgren, Uppsala
• Peter Dybjer, Chalmers          
• Christine Paulin, Paris Sud
• Herman Geuvers, Nijmegen      
• Laurent Thery, INRIA Sophia
• John Harrison, INTEL          
• Freek Wiedijk, Nijmegen
• Per Martin-Lof, Stockholm

• Introduction to Type Theory:
•     Lambda-calculus
•     Propositions-as-types
•     Inductive sets and families of sets
•     Predicative and non-predicative theories
• Foundations:
• Introduction to Systems:
•     Coq
•     Isabelle
•     Agda
• Advanced applications and tools:
•     Proving properties of Java programs
•     Reasoning about Programming Languages
•     Coinduction
•     Correctness of floating-point algorithms
• Dependently typed programming:
•     Dependently typed datastructures
•     Compiling dependent types
• Formalisation of mathematics:
•     Introduction
•     Fundamental theorem of algebra
•     Bishop' set theory
•     Other examples, e.g. prime number theorem

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

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.

Location
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

Organisation
The scientific school directors are

• Alessandro Aldini (University "Carlo Bo", Urbino)
• Roberto Gorrieri (University of Bologna)
• Fabio Martinelli (CNR-IIT, Pisa)

The administrative director is

The local organizer is

Notice and Dates
Prospective participants should apply through the web site by

Notification of accepted applicants will be posted by

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.

Grants
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
        http://www.sti.uniurb.it/events/fosad/
        http://www.sti.uniurb.it/events/fosad05

Sponsors

Under the auspices of:
* EATCS - IT
* EEF
* ERCIM STM WG
* IFIP WG 1.7

• A PhD or equivalent qualifications or experience in an appropriate area of algebra and/or theoretical computer science, preferably some additional research experience, and a track record of publications
• Demonstrable potential to teach undergraduates in pure mathematics and/or computer science, preferably some teaching experience
• Substantial programming experience, preferably including work in computational algebra, and specifically work in GAP
• Knowledge and interests sufficient to contribute to at least two of the projects within the Multidisciplinary Critical Mass grant (in making the two appointments, we will be seeking complementary backgrounds and interests)
• Commitment to multidisciplinary research, in particular to developing and promoting applications of computational algebra in Computer Science, Physics, Mathematics and elsewhere
• Excellent communication, organisational, management and leadership skills.

• Stochastic Constraint Programming
• Robust Constraint Programming
• Optimization
• Supply Chain Uncertainty

Topic

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:

• reasoning about action and change,
• nonmonotonic reasoning,
• description logics and ontologies, and
• action planning.

Registration

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.

Fees

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.

Grants

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.

Assistance

We will provide assistance in finding an accommodation in Dresden.

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.

• Ciao Prolog
• GNU Prolog
• SWI-Prolog
• SICStus Prolog
• YAP

• a library on vectors
• 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

•   Deductive Verification
•   Model Checking
•   Run-Time and Compiler Verification
•   Decision Procedures
•   Static Analysis Techniques
•   Abstract Interpretation
•   Theorem Proving
•   Compositional and Refinement-Based Methodologies
•   Infinite-State Methods

I am delighted to announce the availability of a new book:

  To order direct from Amazon...
    http://www.amazon.com/exec/obidos/ASIN/0262162288/benjamcpierce
  For more information...
    http://www.cis.upenn.edu/~bcpierce/attapl


COVER BLURB:
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

    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:
    http://www.cis.upenn.edu/~bcpierce/attapl