[TYPES/announce] summer school on Coq

[Francesco Zappa Nardelli]

Dear all, I'd like to announce a CEA-EDF-INRIA summer school on:

   Modelling and verifying algorithms in Coq: an introduction

7- 11 juin 2010 - INRIA Paris, France.

Objectives

The Coq system provides a functional programming language and a
reasoning framework based on higher order logic to perform proofs on
the programs. The expressive power of the language is such that
advanced notions of mathematics (such as the graph theory in the four
color theorem) or programs of high complexity (such as a compiler for
a significant kernel of the C Programming language) can be described
formally. In this school, we address the basic programming techniques
and approaches to prove properties of the programs. The covered
notions involve structural recursive programming, list and integer
handling, proof by induction, in the key definition of data-types,
pattern matching constructs and case-based reasoning, and inductive
properties.

Audience

This school is a 5 days course for students, researchers and
engineers. Participants should be familiar with programming (in C,
Java, or ML). Participants are invited to bring their own laptop to
profit of the afternoon exercise sessions.

Speakers

Yves Bertot     INRIA
Pierre Castéran  LABRI, Université de Bordeaux
Pierre Letouzey Université de Paris VII et INRIA
Assia Mahboubi  INRIA

Venue

The school will be held in Paris, France at the new "Antenne
Parisienne" of INRIA (23, avenue d'Italie, 75013 Paris).  The school
fees include lunches but no accommodation in provided.  A list of
hotels is available upon request.

On the web

http://www.inria.fr/actualites/colloques/cea-edf-inria/2010/model-algo/index.en.html
http://www.inria.fr/actualites/colloques/cea-edf-inria/2010/model-algo/programme.en.html

For information, please contact symposia at inria.fr.

Best regards
 Francesco Zappa Nardelli