Coq Winter School (international computer science master, University of Nice)


From Monday January 13 to Friday January 17, 2014, Yves Bertot will be teaching a
course entitled

in the context of the international computer science master at the university of Nice, in Sophia Antipolis.


1/ Basic programming with Coq’s functional programming language.

2/ Handling logical formulas and performing basic proofs.

3/ Reasoning about recursive functions.

4/ Proofs in arithmetic and execution of formally verified programs

5/ General datatypes

Courses will take place from 9:00 to 12:00 and 13:30 to 17:00, every day  of the week, and will alternate lectures with hands-on exercises for all  students.  The course is in English and will at Ecole Polytech’Nice in Sophia Antipolis (approximate geographical coordinate : 43.6155, 7.0719, there is a welcome desk in the building and the room is very close to it).  Rooms change everyday: Monday 317, Tuesday morning 302, Tuesday afternoon 310, Wednesday and Thursday morning 303, Thursday afternoon 308, Friday 307.

This course is an introductory course intended for students in computer  science who have very little knowledge of functional programming and no  knowledge of computer proof.  The background in mathematics will also be  elementary (basically, you are required to know how to perform a division on a sheet of paper and you may learn how to compute a square root).

At the end of the week, we expect that students will know how to write  little programs (for instance number of list manipulations), write  specifications about programs (for instance that a sorting algorithm  does not loose data), and perform the proof that programs satisfy  specifications If you, one of your students, or one of your colleague wishes to learn  about Coq from scratch, this may be the right event for you.

If you are a doctoral student in computer science or mathematics, not  already specializing in computer-based proofs, you will be able to  validate credits for this course, as long as you show up to most of the  sessions during the week.

If you wish to attend, it is preferable that you send a mail to me, so that I can plan the size of the required room and I can warn you about  changes in the organization.