The Coq mailing list

[Yves Bertot <Yves.Bertot AT inria.fr>]

The Marelle team at Inria in Sophia Antipolis is organizing two schools 
on Coq.


1/ A one week advanced school on Coq and Ssreflect
=======================

   ADVANCED SOFTWARE VERIFICATION AND COMPUTER PROOF

in Sophia-Antipolis (Nice) from Monday November 28th, 2016 to Friday 
December 2nd.

The school will be in English and will target master students with
already basic knowledge of Coq.  The course will introduce formalization
techniques based on the SSReflect proof language and the Mathematical
Components library.

All relevant data is at:

https://team.inria.fr/marelle/advanced-coq-winter-school-2016-2017/

--
Cyril Cohen, Laurence Rideau, Enrico Tassi and Laurent Thery




2/ A one week introductory course
=======================

  PROGRAMMING, SPECIFYING, AND PROVING WITH THE COQ SYSTEM

   January 30 -- February 3, 2017

  Inria Sophia Antipolis

  https://team.inria.fr/marelle/coq-winter-school-2017/

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).

At the end of the week, we expect that students will know how to write 
little programs (for instance number or 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.

Registration is free but mandatory and every participant is responsible 
for their own accommodation, but we can provide some help finding 
affordable solutions.  You can register by sending a mail to Nathalie 
Bellesso and Yves Bertot ( firstname.name AT inria.fr ).