From mboxrd@z Thu Jan 1 00:00:00 1970 X-Sympa-To: caml-list@inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p4N4iuYU008407 for ; Mon, 23 May 2011 06:44:56 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: At4AAPHl2U2MbRQxgWdsb2JhbACXZY47FAEBFiYmpECUc4h0gxSDBQSGToEgkG6GNw X-IronPort-AV: E=Sophos;i="4.65,254,1304287200"; d="scan'208";a="95181348" Received: from mx.iis.sinica.edu.tw ([140.109.20.49]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 23 May 2011 06:44:49 +0200 Received: from webmail.iis.sinica.edu.tw ([192.168.0.51]) by mx.iis.sinica.edu.tw (8.14.3/8.14.3) with ESMTP id p4N4ifOH097411 for ; Mon, 23 May 2011 12:44:41 +0800 (CST) (envelope-from bywang@iis.sinica.edu.tw) Received: from webmail.iis.sinica.edu.tw (localhost [127.0.0.1]) by webmail.iis.sinica.edu.tw (8.14.4/8.14.4) with ESMTP id p4N4ifkK072262 for ; Mon, 23 May 2011 12:44:41 +0800 (CST) (envelope-from bywang@iis.sinica.edu.tw) Received: (from www@localhost) by webmail.iis.sinica.edu.tw (8.14.4/8.14.4/Submit) id p4N4ifkI072261 for caml-list@yquem.inria.fr; Mon, 23 May 2011 12:44:41 +0800 (CST) (envelope-from bywang@iis.sinica.edu.tw) X-Authentication-Warning: webmail.iis.sinica.edu.tw: www set sender to bywang@iis.sinica.edu.tw using -f Received: from tu140032.ip.tsinghua.edu.cn (tu140032.ip.tsinghua.edu.cn [166.111.140.32]) by webmail.iis.sinica.edu.tw (Horde Framework) with HTTP; Mon, 23 May 2011 12:44:41 +0800 Message-ID: <20110523124441.15111zzdivifee61@webmail.iis.sinica.edu.tw> Date: Mon, 23 May 2011 12:44:41 +0800 From: bywang@iis.sinica.edu.tw To: caml-list@yquem.inria.fr MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; DelSp="Yes"; format="flowed" Content-Disposition: inline User-Agent: Internet Messaging Program (IMP) H3 (4.3.8) / FreeBSD-8.1 X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-4.2.3 (mx.iis.sinica.edu.tw [192.168.0.49]); Mon, 23 May 2011 12:44:41 +0800 (CST) X-Spam-Score: -1 () ALL_TRUSTED X-Scanned-By: MIMEDefang 2.67 on 192.168.0.49 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id p4N4iuYU008407 X-Validation-by: bywang@iis.sinica.edu.tw Subject: [Caml-list] CPP 2011 - Call for Papers The First International Conference on Certified Programs and Proofs (CPP 2011) CALL FOR PAPERS Kenting, Taiwan December 7--9, 2011 http://formes.asia/cpp (co-located with APLAS 2011) CPP is a new international forum on theoretical and practical topics in all areas, including computer science, mathematics, and education, that consider certification as an essential paradigm for their work. Certification here means formal, mechanized verification of some sort, preferably with production of independently checkable certificates. We invite submissions on topics that fit under this rubric. Suggested, but not exclusive, specific topics of interest for submissions include: certified or certifying programming, compilation, linking, OS kernels, runtime systems, and security monitors; program logics, type systems, and semantics for certified code; certified decision procedures, mathematical libraries, and mathematical theorems; proof assistants and proof theory; new languages and tools for certified programming; program analysis, program verification, and proof-carrying code; certified secure protocols and transactions; certificates for decision procedures, including linear algebra, polynomial systems, SAT, SMT, and unification in algebras of interest; certificates for semi-decision procedures, including equality, first-order logic, and higher-order unification; certificates for program termination; logics for certifying concurrent and distributed programs; higher-order logics, logical systems, separation logics, and logics for security; and teaching mathematics and computer science with proof assistants. INVITED SPEAKERS: * Andrew Appel (Princeton University) * Nikolaj Bjørner (Microsoft Research) * Peter O'Hearn (Queen Mary, University of London) * Vladimir Voevodsky (Institute for Advanced Study, Princeton University) IMPORTANT DATES: Authors are required to submit a paper title and a short abstract before submitting the full paper. The submission should include when necessary a url where to find the formal development assessing the essential aspects of the work. All submissions will be electronic. All deadlines are at midnight (GMT). Abstract Deadline: Monday, June 13, 2011 Paper Submission Deadline: Friday, June 17, 2011 Author Notification: Monday, August 29, 2011 Camera Ready: Monday, September 19, 2011 Conference: December 7-9, 2011 SUBMISSION INSTRUCTIONS: Papers should be submitted electronically online via the conference submission web page at URL: http://www.easychair.org/conferences/?conf=cpp2011 Acceptable formats are PostScript or PDF, viewable by Ghostview or Acrobat Reader. Submissions should not exceed 16 pages in LNCS format, including bibliography and figures. Submitted papers will be judged on the basis of significance, relevance, correctness, originality, and clarity. They should clearly identify what has been accomplished and why it is significant. The proceedings of the symposium will be published as a volume in Springer-Verlag's Lecture Notes in Computer Science series. Each submission must be written in English and provide sufficient detail to allow the program committee to assess the merits of the paper. It should begin with a succinct statement of the issues, a summary of the main results, and a brief explanation of their significance and relevance to the conference, all phrased for the non-specialist. Technical and formal developments directed to the specialist should follow. Whenever appropriate, the submission should come along with a formal development, using whatever prover, e.g., Agda, Coq, Elf, HOL, HOL-Light, Isabelle, Matita, Mizar, NQTHM, PVS, Vampire, etc. References and comparisons with related work should be included. Papers not conforming to the above requirements concerning format and length may be rejected without further consideration. The results must be unpublished and not submitted for publication elsewhere, including the proceedings of other published conferences or workshops. The PC chairs should be informed of closely related work submitted to a conference or journal in advance of submission. Original formal proofs of known results in mathematics or computer science are among the targets. One author of each accepted paper is expected to present it at the conference. AWARD FOR BEST PAPER: An award will be given for the best accepted paper, as judged by the program committee. The committee may decline to make the award or split it among several papers. PROGRAM CO-CHAIRS: Jean-Pierre Jouannaud (INRIA and Tsinghua University) Zhong Shao (Yale University) Email: cpp2011pc@gmail.com GENERAL CHAIR: Yih-Kuen Tsay (National Taiwan University) PROGRAM COMMITTEE: Andrea Asperti (University of Bologna) Gilles Barthe (IMDEA Software Institute) Xiao-Shan Gao (Chinese Academy of Sciences) Georges Gonthier (Microsoft Research Cambridge) Chris Hawblitzel (Microsoft Research Redmond) John Harrison (Intel Corporation) Jean-Pierre Jouannaud (INRIA and Tsinghua University) Akash Lal (Microsoft Research India) Xavier Leroy (INRIA Paris-Rocquencourt) Yasuhiko Minamide (University of Tsukuba) Shin-Cheng Mu (Academia Sinica) Michael Norrish (NICTA) Brigitte Pientka (McGill University) Sandip Ray (University of Texas at Austin) Natarajan Shankar (SRI International) Zhong Shao (Yale University) Christian Urban (TU Munich) Viktor Vafeiadis (Max Planck Institute for Software Systems) Stephanie Weirich (University of Pennsylvania) Kwangkeun Yi (Seoul National University) PUBLICITY CHAIR: Bow-Yaw Wang (Academia Sinica, INRIA and Tsinhua University) ORGANIZING COMMITTEE: Tyng-Ruey Chuang (chair), Shin-Cheng Mu, Yih-Kuen Tsay (Academia Sinica and National Taiwan University) Email: cpp2011oc@gmail.com ---------------------------------------------------------------- This message was sent using IMP, the Internet Messaging Program.