From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 72557BC37 for ; Mon, 1 Mar 2010 09:48:52 +0100 (CET) X-IronPort-AV: E=Sophos;i="4.49,559,1262559600"; d="scan'208";a="45730063" Received: from dizzy.inria.fr (HELO [138.96.196.90]) ([138.96.196.90]) by mail3-relais-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 01 Mar 2010 09:48:52 +0100 Message-ID: <4B8B7F6A.4000605@sophia.inria.fr> Date: Mon, 01 Mar 2010 09:48:42 +0100 From: Yves Bertot User-Agent: Thunderbird 1.5.0.10 (Macintosh/20070221) MIME-Version: 1.0 To: caml-list@inria.fr Subject: CFP: Call for papers, Coq Workshop (Edinburgh, July 9) Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 8bit X-Spam: no; 0.00; coq:01 coq:01 interfacing:01 gregoire:01 herbelin:01 disseminate:98 tactics:98 cfp:01 postscript:01 bertot:01 bertot:01 benjamin:01 calculus:01 gonthier:02 explicitly:02 Please help disseminate this call for papers Two changes in the call for papers: 1/ papers describing experiments in other type theory-based proof assistants are explicitly invited to this workshop, 2/ EPTCS (http://eptcs.org/) has agreed to host the proceedings. Call for papers The Coq workshop will bring together Coq users, developers and contributors. The workshop will be organized from submitted papers, invited talks and a plenary discussion on the evolution and design of Coq. Topics for submitting a paper include: * Experiments with type-theoretic proof assistants * Language or tactics features * Theory and implementation of the Calculus of Inductive Constructions * Applications and experience in education and industry * Tools, platforms built on Coq * Plugins, libraries for Coq * Interfacing with Coq * Formalization tricks and Coq pearls Authors should submit their paper through EasyChair at the following link: http://www.easychair.org/conferences/?conf=coq2 Submitted papers should be in (postscript or) portable document format. Papers should not exceed 12 pages in length in single-column full-page 11pt A4 style. If there is sufficient demand, we will try to organize a time slot for demonstrations. Similarly, we may also organize a session on the lessons learned from teaching Coq. If you are interested, please send a brief proposal. Venue FLoC 2010, Edinburgh, Scotland Important Dates * March 22nd: Deadline for submission of papers * May 1st: Acceptance Notification * May 31st: Final version of articles * July 9th: Workshop in Edinburgh Program Committee * Andrew Appel * Yves Bertot (Chair) * Adam Chlipala * Georges Gonthier * Benjamin Grégoire * Hugo Herbelin * Micaela Mayero * Christine Paulin-Mohring * Bas Spitters