From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 46C8A7FCCB for ; Tue, 7 Apr 2015 15:40:42 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of yrg@pps.univ-paris-diderot.fr) identity=pra; client-ip=209.85.212.176; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yann.regisgianas@gmail.com"; x-sender="yrg@pps.univ-paris-diderot.fr"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of yann.regisgianas@gmail.com designates 209.85.212.176 as permitted sender) identity=mailfrom; client-ip=209.85.212.176; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yann.regisgianas@gmail.com"; x-sender="yann.regisgianas@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-wi0-f176.google.com) identity=helo; client-ip=209.85.212.176; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yann.regisgianas@gmail.com"; x-sender="postmaster@mail-wi0-f176.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0ANAQDM3SNVlLDUVdFcg1pcgxWyQAGNboF6AQ2FeYEtTAEBAQEBARIBAQEBBwsLCRIwhDcLBm8NNwIkEgEFASI1iA0NmC+NK4MtPjGLOJcTCpAZgjgMLxKBMwWOY4YJhg+BHYM3jj01gRWBc2KBPD4xgkMBAQE X-IPAS-Result: A0ANAQDM3SNVlLDUVdFcg1pcgxWyQAGNboF6AQ2FeYEtTAEBAQEBARIBAQEBBwsLCRIwhDcLBm8NNwIkEgEFASI1iA0NmC+NK4MtPjGLOJcTCpAZgjgMLxKBMwWOY4YJhg+BHYM3jj01gRWBc2KBPD4xgkMBAQE X-IronPort-AV: E=Sophos;i="5.11,538,1422918000"; d="scan'208";a="131956097" Received: from mail-wi0-f176.google.com ([209.85.212.176]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 07 Apr 2015 15:40:41 +0200 Received: by wiun10 with SMTP id n10so19164069wiu.1 for ; Tue, 07 Apr 2015 06:40:41 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=mime-version:from:date:message-id:subject:to:content-type; bh=irr2AYu6X1SlznNGmRoA2lb6/d9Mg3EDBNhurl8T1rs=; b=Tno7tRNjSWs+/6hxgSq3omUWAqYODGOe8MTGRT+/RbcjKA799k0McCnBCZu06HwAH/ Bt2LDlBWCvDosGcp9xCN6awKjJkWM/d/n2aXu6qhfrj/uGwHyMtRFcVSz7DrLZACdRK0 G9HfAqYZ5BOTCnq0dBimwXJWT/KXY8RM6ADv17s+fbiqoQ0fAo0aVnQW3KzKHHtGkKHU rCH7l1hF3Fct/ZiP3gGw9eWkrvPG2mbqLb1hU4zdZ2etRWj4F14vtq8mA4aF2vR1cRMq 0WMVv9xoW2ic+oDxjL1CGxMQKrSYPDe82MivuzODsaur3hVfENB7tkOrmUOy2ECWwdmw vCPg== X-Received: by 10.194.2.145 with SMTP id 17mr39426543wju.79.1428414041579; Tue, 07 Apr 2015 06:40:41 -0700 (PDT) MIME-Version: 1.0 From: =?UTF-8?B?WWFubiBSw6lnaXMtR2lhbmFz?= Date: Tue, 07 Apr 2015 13:40:41 +0000 Message-ID: To: "caml-list@inria.fr" Content-Type: multipart/alternative; boundary=047d7b3a896c8a660f0513228fce Subject: [Caml-list] [EPIT15] Call for participation to a spring school about the Coq proof assistant --047d7b3a896c8a660f0513228fce Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable *** 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=3D19&NaiveForm_i= d=3DAzChoixColloque&btnAzurP=3DPreinscription&lang=3Den * Pedagogical committee - Pierre Letouzey (University Paris-Diderot) ; - Arthur Chargu=C3=A9raud (INRIA) ; - Matthieu Sozeau (INRIA) ; - Damien Pous (CNRS) ; - Assia Mahboubi (INRIA) ; - Benjamin Gr=C3=A9goire (INRIA). The school is organized by: - Pierre Letouzey (University Paris-Diderot) ; - Matthieu Sozeau (INRIA) ; - Yann R=C3=A9gis-Gianas (University Paris-Diderot) ; - Pierre-Marie P=C3=A9drot (University Paris-Diderot). If you need any information, please contact Yann R=C3=A9gis-Gianas (yrg at pps.univ-paris-diderot.fr). --047d7b3a896c8a660f0513228fce Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
*** Call for participation, please distribute. ***


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

=C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0Spring School in Theoretical Computer Science

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Mechanizin= g Proofs of Programs in Coq

=C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 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 rese= arch work.

* Program

The = school will take place between May 24 and May 29 and it will be
d= ivided into eight sessions. A session will consist in a (rather
s= hort) 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 theor= y of
rational languages and the computational combinatorics. Fina= lly,
during the last session, participants will work on the mecha= nization
of their specific research domain with the help of the p= edagogical
team of the school.

* Registr= ation

To get more information and to register, ple= ase go to

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0http://www.epit2015.website<= /div>

Registration deadline : April 30, 2015
<= br>
You can register directly by following

https://www.azur-colloque.fr/DR01/AzurInscription/?&iColId= =3D19&NaiveForm_id=3DAzChoixColloque&btnAzurP=3DPreinscription&= lang=3Den

* Pedagogical committee
- Pierre Letouzey (University Paris-Diderot) ;
- Art= hur Chargu=C3=A9raud (INRIA) ;
- Matthieu Sozeau (INRIA) ;
<= div>- Damien Pous (CNRS) ;
- Assia Mahboubi (INRIA) ;
-= Benjamin Gr=C3=A9goire (INRIA).

The school is org= anized by:
- Pierre Letouzey (University Paris-Diderot) ;
- Matthieu Sozeau (INRIA) ;
- Yann R=C3=A9gis-Gianas (Universi= ty Paris-Diderot) ;
- Pierre-Marie P=C3=A9drot (University Paris-= Diderot).

If you need any information, please cont= act Yann R=C3=A9gis-Gianas (yrg at pps.univ-paris-diderot.fr).

--047d7b3a896c8a660f0513228fce--