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 6783C7F102 for ; Tue, 16 Feb 2016 14:53:11 +0100 (CET) IronPort-PHdr: 9a23:jNrU0B2FA9bDolXasmDT+DRfVm0co7zxezQtwd8ZsegVLPad9pjvdHbS+e9qxAeQG96LtLQY0KGL7ejJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6NyZjsnL3ss7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLWKD+OqA5VqBwDTI8Mmlz6te4mwPESF6p53AbVmwN2j9BDAHY4FmuW57+uzb2nvd72TKGJ8SwQ6piCmfq1LtiVBK90HRPDDU+6myC0sE= Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=magaud@unistra.fr; spf=Pass smtp.mailfrom=magaud@unistra.fr; spf=None smtp.helo=postmaster@mailhost.u-strasbg.fr Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of magaud@unistra.fr) identity=pra; client-ip=130.79.222.217; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="magaud@unistra.fr"; x-sender="magaud@unistra.fr"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of magaud@unistra.fr designates 130.79.222.217 as permitted sender) identity=mailfrom; client-ip=130.79.222.217; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="magaud@unistra.fr"; x-sender="magaud@unistra.fr"; 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@mailhost.u-strasbg.fr) identity=helo; client-ip=130.79.222.217; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="magaud@unistra.fr"; x-sender="postmaster@mailhost.u-strasbg.fr"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0DSAgBqKMNWmdneT4JehAxtAYJvtxGCIBcBCYI8gzACgTY8EAEBAQEBAQEBEAEBAQEBCAsJCSEugi2CJxdFKkEDAkgqFAKIBA6NSI04j1uPCh6HfIZWUwmCEgstExiBDwWWf4VTjFOEVIVSjkAPKIFtAVCBUWmHI4E5AQEB X-IPAS-Result: A0DSAgBqKMNWmdneT4JehAxtAYJvtxGCIBcBCYI8gzACgTY8EAEBAQEBAQEBEAEBAQEBCAsJCSEugi2CJxdFKkEDAkgqFAKIBA6NSI04j1uPCh6HfIZWUwmCEgstExiBDwWWf4VTjFOEVIVSjkAPKIFtAVCBUWmHI4E5AQEB X-IronPort-AV: E=Sophos;i="5.22,455,1449529200"; d="scan'208,217";a="203346041" Received: from mailhost.u-strasbg.fr ([130.79.222.217]) by mail2-smtp-roc.national.inria.fr with ESMTP; 16 Feb 2016 14:53:10 +0100 Received: from mailhost.u-strasbg.fr (localhost [127.0.0.1]) by antispam (Postfix) with ESMTP id 99C4D20D0D for ; Tue, 16 Feb 2016 14:53:07 +0100 (CET) X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on mr7.u-strasbg.fr X-Spam-Level: Received: from mailhost.u-strasbg.fr (localhost [127.0.0.1]) by antivirus (Postfix) with ESMTP id 8608720D07 for ; Tue, 16 Feb 2016 14:53:07 +0100 (CET) Received: from lmr.u-strasbg.fr (lmr4.u-strasbg.fr [172.30.21.4]) by mr7.u-strasbg.fr (Postfix) with ESMTP id 6909021EC1 for ; Tue, 16 Feb 2016 14:53:05 +0100 (CET) Received: from lmr.u-strasbg.fr (localhost [127.0.0.1]) by antivirus (Postfix) with ESMTP id 5B2BF11D; Tue, 16 Feb 2016 14:53:02 +0100 (CET) Received: from [172.29.8.247] (wifi-244-138.u-strasbg.fr [130.79.244.138]) (Authenticated sender: magaud) by lmr4.u-strasbg.fr (Postfix) with ESMTPSA id A8698ED; Tue, 16 Feb 2016 14:52:58 +0100 (CET) From: Nicolas Magaud Content-Type: multipart/alternative; boundary="Apple-Mail=_17B9FFC1-BEF0-48C5-9835-FA226A4A587E" Date: Tue, 16 Feb 2016 14:52:58 +0100 To: caml-list@inria.fr Message-Id: <18752A55-A476-4C8B-B6E2-BED60FEA1756@unistra.fr> Mime-Version: 1.0 (Mac OS X Mail 9.2 \(3112\)) X-Mailer: Apple Mail (2.3112) X-Virus-Scanned: ClamAV using ClamSMTP X-Virus-Scanned: ClamAV using ClamSMTP X-Validation-by: magaud@unistra.fr Subject: [Caml-list] The 8th Coq Workshop - 1st CFP --Apple-Mail=_17B9FFC1-BEF0-48C5-9835-FA226A4A587E Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D The Eighth Coq Workshop (2016) http://coq.inria.fr/coq-workshop/2016 Colocated with the 7th International Conference on Interactive Theorem Pr= oving (ITP 2016)=20 August 26, 2016 in Nancy, France =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D The Coq Workshop series brings together Coq users, developers, and contribu= tors. While=20 conferences usually provide a venue for traditional research papers, the Co= q Workshop focuses on strengthening the Coq community and providing a forum for discussing practi= cal issues, including the=20 future of the Coq software and its associated ecosystem of libraries and to= ols. Thus, the workshop will be=20 organized around informal presentations and discussions, likely supplemente= d with invited talks. Submission Instructions=20 We invite all members of the Coq community to propose informal talks, discu= ssion sessions, or any=20 potential uses of the day allocated to the workshop. Relevant subject matt= er includes but is not limited to: * Language or tactic features * Theory and implementation of the Calculus of Inductive Constructions * Applications and experience in education and industry * Tools and platforms built on Coq * Plugins and libraries for Coq * Interfacing with Coq * Formalization tricks and Coq pearls Authors should submit short proposals through EasyChair. Submissions shoul= d be in portable=20 document format (PDF). Proposals should not exceed 2 pages in length in si= ngle-column full-page style. Venue: Nancy, France Important Dates: * June 1: Deadline for proposal submission * June 15: Acceptance notification *August 26: Workshop in Nancy Submission URL: https://www.easychair.org/conferences/?conf=3Dcoq8 Program committee:=20 * Fr=C3=A9d=C3=A9ric Blanqui, INRIA, France * Adam Chlipala, MIT, United States * Cyril Cohen, INRIA, France * Pierre Courtieu, CNAM, France * J=C3=B3nathan Heras Vicente, University of La Rioja, Spain * Robbert Krebbers, Aarhus University, Denmark * Nicolas Magaud (co-chair), University of Strasbourg, France * Micaela Mayero, Univeristy of Paris 7, France * Julien Narboux (co-chair), University of Strasbourg, France * Claudio Sacerdoti-Coen, University of Bologna, Italy * Beta Ziliani, FAMAF, Universidad Nacional de C=C3=B3rdoba, Argentina, and= CONICET, Argentina=20=20=20=20 Organization: Contacts: Nicolas Magaud (magaud@unistra.fr ), Ju= lien Narboux (narboux@unistra.fr )= --Apple-Mail=_17B9FFC1-BEF0-48C5-9835-FA226A4A587E Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D

The Eighth Coq Workshop (2016)
http://coq.inria.fr/coq-workshop/2016

= Colocated with the 7th International Conference on Interactive Theorem Prov= ing (ITP 2016) 
August 26, 2016 in&= nbsp;Nancy, France

=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D

The Coq Workshop series brings t= ogether Coq users, developers, and contributors.  While 
conferences usually provide a venue for traditional research p= apers, the Coq Workshop focuses on
strengthening the C= oq community and providing a forum for discussing practical issues, includi= ng the 
future of the Coq software and its associ= ated ecosystem of libraries and tools.  Thus, the workshop will be&nbs= p;
organized around informal presentations and discuss= ions, likely supplemented with invited talks.

Submission Instructions 

We invite all m= embers of the Coq community to propose informal talks, discussion sessions,= or any 
potential uses of the day allocated to t= he workshop.  Relevant subject matter includes but is not limited to:<= /div>

    &nb= sp;* Language or tactic features
     *= Theory and implementation of the Calculus of Inductive Constructions
=
     * Applications and experience in educat= ion and industry
     * Tools and platf= orms built on Coq
     * Plugins and li= braries for Coq
     * Interfacing with= Coq
     * Formalization tricks and Co= q pearls

Authors = should submit short proposals through EasyChair.  Submissions should b= e in portable 
document format (PDF).  Propo= sals should not exceed 2 pages in length in single-column full-page style.<= /div>

Ven= ue: Nancy, France

Important Dates:

     * June 1: De= adline for proposal submission
     * J= une 15: Acceptance notification
     *A= ugust 26: Workshop in Nancy

Submission URL: https://www.easychair.org/conferences/?conf= =3Dcoq8

Program committee: 

<= /div>
* Fr=C3=A9d=C3=A9ric Blanqui, INRIA, France
* Adam Chlipala, MIT, United States
* Cyril= Cohen, INRIA, France
* Pierre Courtieu, CNAM, France<= /div>
* J=C3=B3nathan Heras Vicente, University of La Rioja,= Spain
* Robbert Krebbers, Aarhus University, Denmark<= /div>
* Nicolas Magaud (co-chair), University of Strasbourg,= France
* Micaela Mayero, Univeristy of Paris 7, Franc= e
* Julien Narboux (co-chair), University of Strasbour= g, France
* Claudio Sacerdoti-Coen, University of Bolo= gna, Italy
* Beta Ziliani, FAMAF, Universidad Nacional= de C=C3=B3rdoba, Argentina, and CONICET, Argentina    

Organization= :

Contacts: N= icolas Magaud (magaud@unist= ra.fr), Julien Narboux (narboux@unistra.fr)
= --Apple-Mail=_17B9FFC1-BEF0-48C5-9835-FA226A4A587E--