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 6B1187F20B; Thu, 7 Feb 2013 16:39:30 +0100 (CET) X-IronPort-AV: E=Sophos;i="4.84,622,1355094000"; d="scan'208";a="1432611" Received: from sac026s.vpn.inria.fr (HELO [138.96.230.26]) ([138.96.230.26]) by mail3-relais-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-CAMELLIA256-SHA; 07 Feb 2013 16:32:31 +0100 Message-ID: <5113CAB1.2030308@inria.fr> Date: Thu, 07 Feb 2013 16:39:29 +0100 From: Assia Mahboubi User-Agent: Mozilla/5.0 (X11; Linux i686; rv:17.0) Gecko/20130106 Thunderbird/17.0.2 MIME-Version: 1.0 To: coq-club@inria.fr, types-announce@lists.seas.upenn.edu, caml-list@inria.fr, "ssreflect@msr-inria.inria.fr" X-Enigmail-Version: 1.5 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit Subject: [Caml-list] The 5th Coq Workshop ================================================================================ The Fifth Coq Workshop (2013) http://coq.inria.fr/coq-workshop/2013 Colocated with the 4rd International Conference on Interactive Theorem Proving (ITP 2013), Rennes, France ================================================================================ The Coq Workshop series brings together Coq users, developers, and contributors. While conferences like ITP 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, likely 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. Relevant subject matter 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 should be in portable document format (PDF). Proposals should not exceed 2 pages in length in single-column full-page style. Venue: ITP, Rennes. Important Dates: * April 7: Deadline for proposal submission * April 28: Acceptance notification * July 22: Workshop in Rennes Submission URL: https://www.easychair.org/conferences/?conf=coq5 Program committee: * Pierre Letouzey, Université Paris 7, France * Marco Maggesi, Università degli Studi di Firenze, Italy * Assia Mahboubi (co-chair), INRIA, France * David Pichardie, INRIA, France * Benjamin Pierce, University of Pennsylvania, USA * Randy Pollack, University of Edinburgh, UK * Enrico Tassi (co-chair), INRIA, France * Viktor Vafeiadis, MPI-SWS, Germany Contact: Assia Mahboubi (assia.mahboubi@inria.fr), Enrico Tassi (enrico.tassi@inria.fr)