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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id E04777F62B for ; Thu, 12 May 2016 10:22:53 +0200 (CEST) IronPort-PHdr: 9a23:ILf5nRRNd3w9nZcL9qrd179PStpsv+yvbD5Q0YIujvd0So/mwa64YRaN2/xhgRfzUJnB7Loc0qyN4/GmADxLsM7JmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbviqtuKM04Z3HKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGefBcqE5S7VCRHR9azh0t4XXskzIRA6Lo38dSXk+kxxSAgGD4gupcI32t37ct+F63CCBdej/QrkpVXz26q5kQQLkoDoBNiUl6miRhNYm3/ETmw6ouxEqmt2cW4qSLvcrJfuFcA== Authentication-Results: mail3-smtp-sop.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 (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of magaud@unistra.fr) identity=pra; client-ip=130.79.222.215; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="magaud@unistra.fr"; x-sender="magaud@unistra.fr"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of magaud@unistra.fr designates 130.79.222.215 as permitted sender) identity=mailfrom; client-ip=130.79.222.215; receiver=mail3-smtp-sop.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 (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mailhost.u-strasbg.fr) identity=helo; client-ip=130.79.222.215; receiver=mail3-smtp-sop.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: A0BhAwCJPDRXitfeT4JegmyBIX0BgnykFJRMIoJAgzICgTM8EAEBAQEBAQEBEQEBAQoLCQkhL4IygiMXRSpBAwJIKhQCiBkOjSGNO49ikRABHYgWhA8BgmFagkorgi4FmCeFfo0BhF6FWo9BDyiBbVAEgVdshnOBPgEBAQ X-IPAS-Result: A0BhAwCJPDRXitfeT4JegmyBIX0BgnykFJRMIoJAgzICgTM8EAEBAQEBAQEBEQEBAQoLCQkhL4IygiMXRSpBAwJIKhQCiBkOjSGNO49ikRABHYgWhA8BgmFagkorgi4FmCeFfo0BhF6FWo9BDyiBbVAEgVdshnOBPgEBAQ X-IronPort-AV: E=Sophos;i="5.24,609,1454972400"; d="scan'208,217";a="177555235" Received: from mailhost.u-strasbg.fr ([130.79.222.215]) by mail3-smtp-sop.national.inria.fr with ESMTP; 12 May 2016 10:22:53 +0200 Received: from mailhost.u-strasbg.fr (localhost [127.0.0.1]) by antispam (Postfix) with ESMTP id 2B40DA293F for ; Thu, 12 May 2016 10:22:52 +0200 (CEST) X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on mr5.u-strasbg.fr X-Spam-Level: Received: from mailhost.u-strasbg.fr (localhost [127.0.0.1]) by antivirus (Postfix) with ESMTP id 19A53A29A3 for ; Thu, 12 May 2016 10:22:52 +0200 (CEST) Received: from local-mr.u-strasbg.fr (lmr3.u-strasbg.fr [172.30.21.3]) by mr5.u-strasbg.fr (Postfix) with ESMTP id 0A8B5A293F for ; Thu, 12 May 2016 10:22:50 +0200 (CEST) Received: from local-mr.u-strasbg.fr (localhost [127.0.0.1]) by antivirus (Postfix) with ESMTP id D594EA4 for ; Thu, 12 May 2016 10:22:50 +0200 (CEST) Received: from [172.29.1.228] (wifi-eduroam-0-23.u-strasbg.fr [130.79.0.23]) (Authenticated sender: magaud) by lmr3.u-strasbg.fr (Postfix) with ESMTPSA id 6B0C8A0 for ; Thu, 12 May 2016 10:22:49 +0200 (CEST) From: Nicolas Magaud Content-Type: multipart/alternative; boundary="Apple-Mail=_DADBB9D0-A89F-478D-9BDD-892AD2DF812A" Message-Id: <223A3F46-3F58-40D5-8E44-923FE1AAF617@unistra.fr> Date: Thu, 12 May 2016 10:22:51 +0200 To: caml-list@inria.fr Mime-Version: 1.0 (Mac OS X Mail 9.3 \(3124\)) X-Mailer: Apple Mail (2.3124) 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 - 2nd CFP - deadline for submission: june 1st 2016 --Apple-Mail=_DADBB9D0-A89F-478D-9BDD-892AD2DF812A 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=_DADBB9D0-A89F-478D-9BDD-892AD2DF812A 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
     * = August 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= : Nicolas Magaud (magaud@un= istra.fr), Julien Narboux (narboux@unistra.fr)

= --Apple-Mail=_DADBB9D0-A89F-478D-9BDD-892AD2DF812A--