[Caml-list] [Second call for participation] Spring School about Proofs of Programs using Coq

["Yann Régis-Gianas" <yrg@pps.univ-paris-diderot.fr>]

[-- Attachment #1: Type: text/plain, Size: 2308 bytes --]

*** Call for participation, please distribute. ***


              EPIT'2015 (http://www.epit2015.website)

           Spring School in Theoretical Computer Science

              Mechanizing Proofs of Programs in Coq

              May 25 to May 29, 2015, Frejus, France


* Presentation

The french spring school in theoretical computer science (EPIT) is a
recurrent school which was created 40 years ago by Maurice Nivat.
This year, the school is about the mechanization of proofs of programs
using the proof assistant Coq. As no prerequisite is needed, the
school targets any computer scientist that is curious about what a proof
assistant is and how it can be integrated in its daily research work.

* Program

The school will take place between May 24 and May 29 and it will be
divided into eight sessions. A session will consist in a (rather
short) lecture (given in english) followed by practical exercises on
computer. The five first sessions will be dedicated to a presentation
of the main concepts and techniques used to mechanize proofs on a
computer. The two next sessions will focus on the mechanization of two
classical domains of theoretical computer science: the theory of
rational languages and the computational combinatorics. Finally,
during the last session, participants will work on the mechanization
of their specific research domain with the help of the pedagogical
team of the school.

* Registration

To get more information and to register, please go to

           http://www.epit2015.website

Registration deadline : April 30, 2015

You can register directly by following

https://www.azur-colloque.fr/DR01/AzurInscription/?&iColId=19&NaiveForm_id=AzChoixColloque&btnAzurP=Preinscription&lang=en

* Pedagogical committee

- Pierre Letouzey (University Paris-Diderot) ;
- Arthur Charguéraud (INRIA) ;
- Matthieu Sozeau (INRIA) ;
- Damien Pous (CNRS) ;
- Assia Mahboubi (INRIA) ;
- Benjamin Grégoire (INRIA).

The school is organized by:
- Pierre Letouzey (University Paris-Diderot) ;
- Matthieu Sozeau (INRIA) ;
- Yann Régis-Gianas (University Paris-Diderot) ;
- Pierre-Marie Pédrot (University Paris-Diderot).

If you need any information, please contact Yann Régis-Gianas (yrg at
pps.univ-paris-diderot.fr).

[-- Attachment #2: Type: text/html, Size: 3393 bytes --]