* [Caml-list] [EPIT15] Call for participation to a spring school about the Coq proof assistant
@ 2015-04-07 13:40 Yann Régis-Gianas
0 siblings, 0 replies; only message in thread
From: Yann Régis-Gianas @ 2015-04-07 13:40 UTC (permalink / raw)
To: caml-list
[-- 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: 3329 bytes --]
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2015-04-07 13:40 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2015-04-07 13:40 [Caml-list] [EPIT15] Call for participation to a spring school about the Coq proof assistant Yann Régis-Gianas
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox