[TYPES/announce] Two schools on Coq : (Nov 28, 2016) and (Jan 2017), Sophia Antipolis, France
Yves Bertot
Yves.Bertot at inria.fr
Tue Oct 25 02:45:23 EDT 2016
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 ).
More information about the Types-announce
mailing list