The Coq mailing list

[Francesco Zappa Nardelli <francesco.zappa_nardelli AT inria.fr>]

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

  Modelling and verifying algorithms in Coq: an introduction

14-18 November 2011 - 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 engineers and students/researchers.
Participants should be familiar with programming (e.g. in C or Java), 
but no knowledge of a proof assistant or of a functional language is required.
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
Benjamin Gregoire, INRIA
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://moscova.inria.fr/~zappa/teaching/coq/ecole11/

To register

As the number of participants is limited, a pre-registration before 
September 15 is mandatory.  The web page above details the
registration procedure.

Best regards
Francesco Zappa Nardelli