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 c5ff346549e7 (Postfix) with ESMTPS id 902685D5 for ; Wed, 5 Jun 2019 10:48:49 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.60,550,1549926000"; d="scan'208";a="386080756" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 05 Jun 2019 12:48:48 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 6BD8C8247D; Wed, 5 Jun 2019 12:48:48 +0200 (CEST) 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 E97C78247D for ; Wed, 5 Jun 2019 12:48:41 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=garrigue@math.nagoya-u.ac.jp; spf=None smtp.mailfrom=garrigue@math.nagoya-u.ac.jp; spf=None smtp.helo=postmaster@ms.math.nagoya-u.ac.jp IronPort-PHdr: =?us-ascii?q?9a23=3AZ//eIRLZPIvq/JHWlNmcpTZWNBhigK39O0sv0rFi?= =?us-ascii?q?tYgfLfrxwZ3uMQTl6Ol3ixeRBMOHsqsC0raM+Pu5EUU7or+5+EgYd5JNUxJXwe?= =?us-ascii?q?43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRp?= =?us-ascii?q?OOv1BpTSj8Oq3Oyu5pHfeQpFiCegbb9oMRm7ohvdusYYjId/N6081gbHrnxUdu?= =?us-ascii?q?pM2GhmP0iTnxHy5sex+J5s7SFdsO8/+sBDTKv3Yb02QaRXAzo6PW814tbrtQTY?= =?us-ascii?q?QguU+nQcSGQWnQFWDAXD8Rr3Q43+sir+tup6xSmaIcj7Rq06VDi+86tmTgLjhT?= =?us-ascii?q?wZPDAl7m7Yls1wjLpaoB2/oRx/35XUa5yROPZnY6/RYc8WSW9HU81MVSJOH5m8?= =?us-ascii?q?YpMPAeUdMuhXoJTzqVgAoxWgAgehH//vyiZNhnPq3a02z+YsHAfb1wIgBdIOt3?= =?us-ascii?q?HUoc3xOqgITe+11bTIwivYb/hL2Dny8pLIcgogofGDQLJ/b9faxE4gFwzflFWQ?= =?us-ascii?q?s43lPzyI1usTqGWb6vBvVf6vi2I9rQF+uDevxsAsi4bTn44V10rI+j9lz4ovJ9?= =?us-ascii?q?24UFd2bNi5G5VesCGaMpF5QsIkQ2xwoCY117IHtYSlcycX1ZQr3x/fa/qdc4iJ?= =?us-ascii?q?+B3vTuiRIS1giH17Yr2/nBaz/lSgyuLmV8m0ykxGri1fktnDrnwCzR3T6tObSv?= =?us-ascii?q?dn8Ueh3iyD1wLL6u1cJ0A7j6XbK5khw7Eqj5YTrF7PETXql0nsjq+WbkMp8fWr?= =?us-ascii?q?5eT/erjqu5GROoFuhgz/KKgih8KyDfgiPgQTQmSX4eSx2b758UHkQLhHjec6nr?= =?us-ascii?q?THvJ3ZP8gXu660Dg1T340+8RiwFS2m384dnXQfLFJKZhaHj4/xNlHLO/D0F/K/?= =?us-ascii?q?jE6wkDdr3fzGOKfuAprKLnnDirjtZKt951RGxwUv19xf5YpUBqkAIPL1REDxqM?= =?us-ascii?q?TVAgI3PgG62erqCc9x2p4QVG6TGKOVLb7evUeN5u01IumMYIEVuCz6K/gg//Pu?= =?us-ascii?q?gmU2mUUHfamo0psXdW63E+9jI0qDfXrsgs0NEWEQsQoxS+zriEeNXSdOZ3qoRa?= =?us-ascii?q?0z+is3CIC+DYvbXICinKSB3DunHp1Rfm1JFkqDEXLsd4mdX/cMaTmSItN6nzwf?= =?us-ascii?q?VbmhTpch2gu0uA/7zbpnNOvU9TcCuZLtztgmr9HUwDQ79Dh1CcvV92CWUylTtW?= =?us-ascii?q?oNQ3di16l6pQl5y0yf+al+mf1RU9JJsaBnSAA/YLzVxPVnBsu6dQvbZNaGVVvu?= =?us-ascii?q?FtqvGyswQc8869oHf0Y7HdytiQHKmjfsCrRTlaTdV898yb7Vw3Wkf5U18H3Bzq?= =?us-ascii?q?R0ygB+GpIeZ13jvbZ28k3oP6CMlkyYk6iwcqFGhXzI/XuDi2yHs0ZJWUttF6zO?= =?us-ascii?q?G3IHNBOP8YbJo3jaRrrrMowJdxNbwJTbeK5Ddt2vi1xJQ+bqfcmYamn3mX/iXU?= =?us-ascii?q?/VlIPJV5LjfiAm5AuYCEUAlFpPr3Odcw03GifnpWvRCy1nUE+pakiq8/Es8H4?= =?us-ascii?q?=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0C9AgBAnfdclwuCBoVmHAEBAQQBAQcEA?= =?us-ascii?q?QGBZYJ7A08gEiiEFIh7pnMBCAEDAQwjDAEBgUuCdYJyBgY0EwEDAQEEAQECAQE?= =?us-ascii?q?DARMBAQEBAQgWBkwMgjopAYMKBh0BASYRATQCJgJfJwKDDAGCCRClFXGBMYJ5A?= =?us-ascii?q?QEFgkeCbyGBTgmBDCiLcoF/gREnH4FghAsBAxiBIIMxMoImiQcHizKUVAmCEII?= =?us-ascii?q?ahCiMeBuDDIMQhlmKCQGUIIwYgy6BZoF5TThlAYJBCTVZeBqEQFSBSIIOhT4QM?= =?us-ascii?q?DMBjUyCUgEB?= X-IPAS-Result: =?us-ascii?q?A0C9AgBAnfdclwuCBoVmHAEBAQQBAQcEAQGBZYJ7A08gEii?= =?us-ascii?q?EFIh7pnMBCAEDAQwjDAEBgUuCdYJyBgY0EwEDAQEEAQECAQEDARMBAQEBAQgWB?= =?us-ascii?q?kwMgjopAYMKBh0BASYRATQCJgJfJwKDDAGCCRClFXGBMYJ5AQEFgkeCbyGBTgm?= =?us-ascii?q?BDCiLcoF/gREnH4FghAsBAxiBIIMxMoImiQcHizKUVAmCEIIahCiMeBuDDIMQh?= =?us-ascii?q?lmKCQGUIIwYgy6BZoF5TThlAYJBCTVZeBqEQFSBSIIOhT4QMDMBjUyCUgEB?= X-IronPort-AV: E=Sophos;i="5.60,550,1549926000"; d="scan'208";a="386080727" X-MGA-submission: =?us-ascii?q?MDEpjwKCQ6bVjLcve0feqMdizgRaTv2cSxkipL?= =?us-ascii?q?7Z8Aw0JRgsncUF9g907kAi7hcuWsaRzmJEhCNxNDr59TlAVbNyZnniiM?= =?us-ascii?q?orJ9ozwbLDmlN95EMjFv/ZnyfCEeEi2LruXnydJl2bH65Uuwm5y+B4Gm?= =?us-ascii?q?RXgBXqfoZblhqf2Au3SzQHzQ=3D=3D?= Received: from bsd20.math.nagoya-u.ac.jp (HELO ms.math.nagoya-u.ac.jp) ([133.6.130.11]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 05 Jun 2019 12:48:39 +0200 Received: from [192.168.0.12] (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ms.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 907677B9D71; Wed, 5 Jun 2019 19:48:36 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=math.nagoya-u.ac.jp; s=20160220; t=1559731716; bh=T9KGk81k4+DQN3/xw9VEY5gJEozoaIh9ihaGMhbJeAY=; h=From:Subject:Date:Cc:To; b=Izle3FCdTiax2naNPjTjpKoM4ATJM6n8TMLkosnIbSFUfb6mWCBqrZOnmiemPQM+P +vlRCy2bFMu1LDHBiTtuxU20KWLKusqO/gIQUa3CQyYyjwgjZR5r/0a2TwccVXxobg DeywfYOcDY1g9Vf4gVQ2fKZB4fbHrp0ySvAShKbg= From: Jacques Garrigue Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Mime-Version: 1.0 (Mac OS X Mail 12.4 \(3445.104.11\)) Message-Id: <0CDC68FE-713F-4E44-AE7D-CD3640418EE9@math.nagoya-u.ac.jp> Date: Wed, 5 Jun 2019 19:48:25 +0900 Cc: Reynald AFFELDT To: Mailing List OCaml X-Mailer: Apple Mail (2.3445.104.11) X-Greylist: Sender succeeded SMTP AUTH, not delayed by milter-greylist-4.6.2 (ms.math.nagoya-u.ac.jp [0.0.0.0]); Wed, 05 Jun 2019 19:48:36 +0900 (JST) X-Virus-Scanned: clamav-milter 0.99.2 at bsdserver20 X-Virus-Status: Clean X-Spam-Checker-Version: SpamAssassin 3.4.1 (2015-04-28) on bsdserver20.math.nagoya-u.ac.jp Subject: [Caml-list] [CFP] The Coq Workshop 2019 (Deadline Extension) Reply-To: Jacques Garrigue X-Loop: caml-list@inria.fr X-Sequence: 17603 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: The submission deadline has been extended to Monday 2019-06-10. For more information: https://staff.aist.go.jp/reynald.affeldt/coq2019/. -- ********************************************************************* The Coq Workshop 2019: Call for Talk Proposals Colocated with the 10th International Conference on Interactive Theorem Proving (ITP 2019), Portland, OR, USA ********************************************************************** We are pleased to invite you to submit talk proposals for the Coq workshop 2019, which will be held on September 8 2019, in Portland, OR, USA. The Coq workshop is part of ITP 2019 (https://itp19.cecs.pdx.edu/). The Coq workshop 2019 is the 10th Coq Workshop. The Coq Workshop series (https://coq.inria.fr/coq-workshop/) brings together Coq (https://coq.inria.fr/) users, developers, and contributors. While conferences usually provide a venue for traditional research papers, the Coq Workshop focuses on strengthening the Coq community and providing a forum for discussing practical issues, including the future of the Coq software and its associated ecosystem of libraries and tools. Thus, the workshop will be organized around informal presentations and discussions, supplemented with invited talks. We invite all members of the Coq community to propose informal talks, discussion sessions, or any potential uses of the day allocated to the workshop. Important dates: - June 10 2019: Deadline for abstract submission (Extended) - July 2 2019: Notification to authors - September 8 2019: Workshop Submission Instructions: Authors should submit short proposals through EasyChair (https://easychair.org/conferences/?conf=3Dcoq2019) in the form of a PDF extended abstract of less than 2 pages, in full-page single-column style. Relevant subject matter includes but is not limited to: - Theory and implementation of the Calculus of Inductive Constructions - Language or tactic features - Plugins and libraries for Coq - Techniques for formalization programming languages and mathematics - Applications and experience in education and industry - Tools and platforms built on Coq (including interfaces) - Formalization tricks and pearls Program Committee: - Reynald Affeldt (AIST) - Christian Doczkal (CNRS - LIP, ENS Lyon) - Jacques Garrigue (Nagoya University) - Chantal Keller (LRI, Univ. Paris-Sud) - Dominique Larchey-Wendling (CNRS, Loria) - Gregory Malecha (BedRock Systems Inc.) - Pierre-Marie P=C3=A9drot (INRIA) - Ilya Sergey (Yale-NUS College and NUS School of Computing) - John Wiegley (DFINITY) Organization contact (co-chairs): reynald.affeldt AT aist.go.jp, garrigue AT math.nagoya-u.ac.jp