Sites Inria

Version française

CEA-EDF-Inria School

Modelling and verifying algorithms in Coq: an introduction

This school is a 5 days course for engineers, and for students and 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.

  • Date : 14/11/2011 to 18/11/2011
  • Place : Rooms Orange 1 and Orange 2 (5th floor), Inria Antenne de Paris, 23 avenue d'Italie, 75013 Paris. Metro: Place d'Italie.
  • Organiser(s) : Yves Bertot, Pierre Castéran, Pierre Letouzey, Assia Mahboubi

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.

Programme:

Classes will begin on Monday 7 June at 10:00 am, and will end on Friday 11 June at 4:00 pm.

Monday

Elements of typed functional programming: programming without side-ffects, pattern matching, anonymous functions, simple types, higher order functions, recursive functions.

Tuesday

Construction and proof of logical formulas, quantifiers and connectives, equality, predicates on numbers and lists. Goal-directed proofs.

Wednesday

Verification of simple logical formulas on programs. Proofs by induction. Data-types and associated reasoning principles.

Thursday

Inductive predicates and introduction to dependent types. Functions and pattern matching in presence of dependent types.

Friday

Case studies.

As the number of participants is limited, a pre-registration is mandatory. In the pre-registration you are encouraged to briefly explain why you should and wish to attend the summer school. Based on this, all applications will be reviewed with due regard to find a fair distribution of the 30 places among all qualified applicants. Applicants from industry are strongly encouraged to apply.

To pre-register, please fill in this form before September 15. All applicants will receive notice by September 20. Every person who is admitted to attend the summer school must then register before October 1.

Registration fees:

  • Inria members: free
  • Students: 100 euros
  • Academy: 300 euros
  • Full rate: 600 euros

These include attendance to the school and lunches for days 1-5.

Keywords: Algorithms Formal methods The Coq proof assistant

Top