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 38A845D6 for ; Thu, 1 Aug 2019 00:55:18 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.64,332,1559512800"; d="scan'208";a="394055004" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 01 Aug 2019 02:55:17 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 412FE82717; Thu, 1 Aug 2019 02:55:17 +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 1FF2E826BB for ; Thu, 1 Aug 2019 02:55:12 +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=3Axv4z5BHMcfpm09OP2PxKVZ1GYnF86YWxBRYc798d?= =?us-ascii?q?s5kLTJ7yo8mwAkXT6L1XgUPTWs2DsrQY0rCQ4v6rAjJIyK3CmUhKSIZLWR4BhJ?= =?us-ascii?q?detC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+?= =?us-ascii?q?KPjrFY7OlcS30P2594HObwlSizexfK1+IA+yoAjQucUbj4pvIbstxxXUpXdFZ/?= =?us-ascii?q?5Yzn5yK1KJmBb86Maw/Jp9/ClVpvks6c1OX7jkcqohVbBXAygoPG4z5M3wqBnM?= =?us-ascii?q?VhCP6WcGUmUXiRVHHQ7I5wznU5jrsyv6su192DSGPcDzULs5Vyiu47ttRRT1ky?= =?us-ascii?q?oMKSI3/3/LhcxxlKJboQyupxpjw47PfYqZMONycr7Bcd8GQGZMWNtaWS5cDYOm?= =?us-ascii?q?d4YBD/YOM+lXoIfgpFUAowWwCw63CePz0z9Ig2P63a0m3+kjFwzNwQwuH8gJsH?= =?us-ascii?q?TRtNj7ML0dXvyszKnV0zrDdO5d1zbn54jSaBAhoP6MXa9ufsHMzkQvGBnKjk+K?= =?us-ascii?q?qYzkMDOVy/oCvnOe7+V6SeKvi3QrqwdrrTigwcctipPGipsIylze7yp23Jw5Jd?= =?us-ascii?q?+gSENiZ9OvDZVetyafN4RsQ8MiRXlluD4nxbwJo5K0YjUFyIk/yx7ebfyHaYmI?= =?us-ascii?q?7Qj5WOafOzd0nGhqeLOkhxau60Sgxer8WtO20FZStiZFlMPDtn8K1x3T8MeLU+?= =?us-ascii?q?Z98l271jmTzQzT6PlELEYpnqTYM54s2qM8m5QdvEjZHyL6glj6gaGKekk+5+Sk?= =?us-ascii?q?9vzrb7Xlq5OGKoN5igLzPr4zlsChAuk0KBUCUmiZ9Om6ybbt51f2QK9Qgf0ziq?= =?us-ascii?q?TZsI7VJcAcpqOhBg9VyZwv6xOlADe60NQUh38HI0hKeBKAj4nmIUjCIO3iAfil?= =?us-ascii?q?n1ugijVrx+jeMr3gBJXCMGTDna/8cbtz5UNQ0gs+wcpC659aFr0NOu//VlLpuN?= =?us-ascii?q?zdFBA5Mgi0w+j9CNV604MTQW2PDbWDMKPIsF+I6f8vLPeXaY8Qojn9N/gl6+To?= =?us-ascii?q?jXAjll8deqmo0oEOZHClBPhpOVmWbWDugtcZCWsKpBYxTPT2iF2eVj5ef2q9UL?= =?us-ascii?q?g55jE/EY6mCYbDRpuxgLGaxye6HphWZnhcBVyWEHfocZ+EW/YWZy6ILM9hiG9M?= =?us-ascii?q?ab/0boYg0RCou0feyqF7Zs3/8ygc/cbo3d1xounSjg0a9DpuDs3b3XvbHE9umW?= =?us-ascii?q?ZdZTY9xb1yugRSw02Z0KdljrQMGtVJ/fJGTwoSMJfAz6p8At/1SwuEY5GAQxCk?= =?us-ascii?q?WoP1UnkKUtstzopWMA5GENK4g0WGhnLyWuNHp/mwHJUxt5nk8T3pPc8nkiTD3b?= =?us-ascii?q?UhyV8vTcxePCi7wKd0sQrLVdaQwhep0p2yfKFZ5xbjsWKKzG6ApkZdClciVKzZ?= =?us-ascii?q?XTYZb0TRvN28+wXLRPmsEeZ/a1YT+Yu5MqJPL+bRoxBGSfPkYoiMZnn3nm6sBV?= =?us-ascii?q?COz7yLfYOvZiMU12PfEBpcng=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AqAwB7N0JdlwuCBoVmHAEBAQQBAQcEA?= =?us-ascii?q?QGBZ4MFA08gEiqEHoh8o00BCAEDAQwjDAEBgUuCdYJrBgY0EwEDAQEEAQECAQM?= =?us-ascii?q?DARMBAQEBAQgWBoVODII6KQGDCgYdAQEmEQE0AiYCXyeDDgGCCRCrNHGBMoJ6A?= =?us-ascii?q?QEFgkeCcyGBUgmBDCiLd4F/gREnH4FgPoNNAYRtMoImiUwHgmIniG2VSgmCHII?= =?us-ascii?q?fhD2NPRuDG4MlhnyKWpUQjQeDNYFngXlNOGUBgkEJNYIEGoRBVIFIh1wwMwGMd?= =?us-ascii?q?yuCJQEB?= X-IPAS-Result: =?us-ascii?q?A0AqAwB7N0JdlwuCBoVmHAEBAQQBAQcEAQGBZ4MFA08gEiq?= =?us-ascii?q?EHoh8o00BCAEDAQwjDAEBgUuCdYJrBgY0EwEDAQEEAQECAQMDARMBAQEBAQgWB?= =?us-ascii?q?oVODII6KQGDCgYdAQEmEQE0AiYCXyeDDgGCCRCrNHGBMoJ6AQEFgkeCcyGBUgm?= =?us-ascii?q?BDCiLd4F/gREnH4FgPoNNAYRtMoImiUwHgmIniG2VSgmCHIIfhD2NPRuDG4Mlh?= =?us-ascii?q?nyKWpUQjQeDNYFngXlNOGUBgkEJNYIEGoRBVIFIh1wwMwGMdyuCJQEB?= X-IronPort-AV: E=Sophos;i="5.64,332,1559512800"; d="scan'208";a="394054994" X-MGA-submission: =?us-ascii?q?MDFoken1Zo2cqfsFPajW7GrhvORIad7sJ7SyEZ?= =?us-ascii?q?Yst6vNRuh2BRwh3gqMMPu4pb3myURFIVfcp8XsYeC4rjGsD2x7xPrjKs?= =?us-ascii?q?TwRaag5mANTYcnqiXUzyL04cztqJ3TRaRDiMzeu+MNJYB5s/uuuKavpO?= =?us-ascii?q?PwUFR76tUhdzj4D1sMfI5F9w=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; 01 Aug 2019 02:55:10 +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 28528BD7683; Thu, 1 Aug 2019 09:55:07 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=math.nagoya-u.ac.jp; s=20160220; t=1564620907; bh=jZLG7YUsMhvdqSZDe89l0sPaTegO853Ibegvy0PJYFI=; h=From:Subject:Date:Cc:To; b=J0YlRa9hPKvpd0UoQGtbacyAaaGTa/GxFlQIpbi25wW08iyGrmIN/MiTUT4bi3yex ItWm4Kyi5y+nP5+SGaZksJvLdeW+ll9/eekX+8lk2WF9UpVRqf50DWQu031SUik3aZ Z2FjAzoS7j6Zkq4EBjaIa0O7J3FRjiUTwqSgbjGs= 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: <366512BC-8D08-41C8-A8BF-93E1C347CC08@math.nagoya-u.ac.jp> Date: Thu, 1 Aug 2019 09:54:23 +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]); Thu, 01 Aug 2019 09:55:07 +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] [Call for Participation] The Coq Workshop 2019 Reply-To: Jacques Garrigue X-Loop: caml-list@inria.fr X-Sequence: 17729 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 Coq Workshop 2019: Call for Participation Colocated with the 10th International Conference on Interactive Theorem Proving (ITP 2019), Portland, OR, USA ********************************************************************** We are pleased to invite you to participate in 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/). Topic: - 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. Program: - Invited talk: + Nicolas Tabareau: Not a single proof assistant for all, but proof = assistants for everyone - Discussion session with the Coq development team - Accepted talks: + Kazuhiko Sakaguchi. Validating Mathematical Structures + Akira Tanaka. A Gallina Subset for C Extraction of Non-structural = Recursion + Christian Doczkal and Damien Pous. Graph Theory in Coq: Minors, = Treewidth, and Isomorphisms + Bruno Bernardo, Rapha=C3=ABl Cauderlier, Basile Pesin, Zhenlei Hu and = Julien Tesson. Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts + Reynald Affeldt, Jacques Garrigue, Xuanrui Qi and Kazunari Tanaka. Experience Report: Type-Driven Development of Certified Tree = Algorithms in Coq + Enrico Tassi and Erik Martin-Dorel. SSReflect in Coq 8.10 + Matthieu Sozeau, Yannick Forster, Simon Boulier, Nicolas Tabareau and = Th=C3=A9o Winterhalter. Coq Coq Codet! + Florian Steinberg and Holger Thies. Computable analysis, exact real arithmetic and analytic functions in = Coq + Florian Steinberg. _Some formal proofs about summable sequences in = Coq - See https://staff.aist.go.jp/reynald.affeldt/coq2019/ for the = schedule. Registration: - Early registration is before [2019-08-04 Sun] - See the ITP 2019 website for registration information: https://itp19.cecs.pdx.edu/registration/ 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