From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr 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 6D5AF7FD03; Wed, 22 Apr 2015 07:17:48 +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.175; 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.175 as permitted sender) identity=mailfrom; client-ip=209.85.212.175; 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-f175.google.com) identity=helo; client-ip=209.85.212.175; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yann.regisgianas@gmail.com"; x-sender="postmaster@mail-wi0-f175.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0CxAQB0LTdVm6/UVdFbDoNQXIMYtGgBjXaBeAENhgCBOjsRAQEBAQEBAREBAQEBAQYLCwkULoQ5CwZvDTcCJBIBBQEiATSICQ2ZLJBbPjGLOJUeIAqQLYI4DC8SgTMFjxOGIYYogSKDPI8FNYEVgll/PT4xgkQBAQE X-IPAS-Result: A0CxAQB0LTdVm6/UVdFbDoNQXIMYtGgBjXaBeAENhgCBOjsRAQEBAQEBAREBAQEBAQYLCwkULoQ5CwZvDTcCJBIBBQEiATSICQ2ZLJBbPjGLOJUeIAqQLYI4DC8SgTMFjxOGIYYogSKDPI8FNYEVgll/PT4xgkQBAQE X-IronPort-AV: E=Sophos;i="5.11,621,1422918000"; d="scan'208";a="136144953" Received: from mail-wi0-f175.google.com ([209.85.212.175]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 22 Apr 2015 07:17:47 +0200 Received: by wiun10 with SMTP id n10so43922312wiu.1; Tue, 21 Apr 2015 22:17:47 -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=qiWE9tumxDObAELufTw/3btnfCzVsfl8WlYjFayk90c=; b=Reb8/Q0/FGSWNBndhMFvalEVmzMwuNb25XrSzscjWVTUL0txA51zW4r1ZC79kSTl2B 955WqKXlp7R3UqEb8JzGL1nDETdsDiLi+y6fFU2xbsf/7UDN8bC2pJKPROGxwoZ+o0RT WbcLw5EhU8hhtbTfDI0YhIx6w9gDxVDXTKBBrjvQ9SmGD7YNhCe3HxvCrixkXi/lukt7 20qsJMRju6R8S/HqKPp289B5mXQNQACYfIf+IzSOtYfmW4tskAhp9tiP++PL3xvQWIVN oOXkN6yaV/HVoZYT7IcZodzQaQecCdNDpq6vzyBRUCJ8xyCYpC4CHZUFSh2P8YayZlPa iSOg== X-Received: by 10.180.88.99 with SMTP id bf3mr2453058wib.75.1429679867350; Tue, 21 Apr 2015 22:17:47 -0700 (PDT) MIME-Version: 1.0 From: =?UTF-8?B?WWFubiBSw6lnaXMtR2lhbmFz?= Date: Wed, 22 Apr 2015 05:17:46 +0000 Message-ID: To: "caml-list@inria.fr" , "haskell@haskell.org" , "types-announce@lists.seas.upenn.edu" , "coq-club@inria.fr" Content-Type: multipart/alternative; boundary=f46d04428eaea2d60905144948ef Subject: [Caml-list] [Second call for participation] Spring School about Proofs of Programs using Coq --f46d04428eaea2d60905144948ef 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). --f46d04428eaea2d60905144948ef 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 Mechanizing 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, Freju= s, France


* Presentation
=
The french spring school in theoretical computer science (EP= IT) is a
recurrent school which was created 40 years ago by Mauri= ce Nivat.
This year, the school is about the mechanization of pro= ofs of programs
using the proof assistant Coq. As no prerequisite= is needed, the
school targets any computer scientist that is cur= ious about what a proof
assistant is and how it can be integrated= in its daily research work.

* Program
<= br>
The school will take place between May 24 and May 29 and it w= ill be
divided into eight sessions. A session will consist in a (= rather
short) lecture (given in english) followed by practical ex= ercises on
computer. The five first sessions will be dedicated to= a presentation
of the main concepts and techniques used to mecha= nize proofs on a
computer. The two next sessions will focus on th= e mechanization of two
classical domains of theoretical computer = science: the theory of
rational languages and the computational c= ombinatorics. 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 an= d to register, please go to

=C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0http://www.epit2015.website

Registration de= adline : April 30, 2015

You can register directly = by following


* Pedagogical committee

- Pierre = Letouzey (University Paris-Diderot) ;
- Arthur Chargu=C3=A9raud (= INRIA) ;
- Matthieu Sozeau (INRIA) ;
- Damien Pous (CNR= S) ;
- Assia Mahboubi (INRIA) ;
- Benjamin Gr=C3=A9goir= e (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-Gi= anas (yrg at pps.univ-paris-diderot.fr).

--f46d04428eaea2d60905144948ef--