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 mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 5F489BC57 for ; Mon, 21 Jun 2010 18:15:01 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgIGAKYsH0yB1w3NYGdsb2JhbACSX4wlCx8lBR3DbIUbBA X-IronPort-AV: E=Sophos;i="4.53,453,1272837600"; d="scan'208";a="65039828" Received: from nougat.ucs.ed.ac.uk ([129.215.13.205]) by mail4-smtp-sop.national.inria.fr with ESMTP; 21 Jun 2010 18:15:01 +0200 Received: from lmtp1.ucs.ed.ac.uk (lmtp1.ucs.ed.ac.uk [129.215.149.64]) by nougat.ucs.ed.ac.uk (8.13.8/8.13.4) with ESMTP id o5LGF0JY019203 for ; Mon, 21 Jun 2010 17:15:00 +0100 (BST) Received: from haggis.inf.ed.ac.uk (haggis.inf.ed.ac.uk [129.215.24.23]) by lmtp1.ucs.ed.ac.uk (8.13.8/8.13.7) with ESMTP id o5LGF0xc000910 for ; Mon, 21 Jun 2010 17:15:00 +0100 (BST) Message-ID: <4C1F9004.1070201@inf.ed.ac.uk> Date: Mon, 21 Jun 2010 17:15:00 +0100 From: Lucas Dixon User-Agent: Thunderbird 2.0.0.24 (X11/20100317) MIME-Version: 1.0 To: caml-list@inria.fr Subject: PLMMS-2010 call for participation References: <4C1F3F41.8040804@inf.ed.ac.uk> In-Reply-To: X-Enigmail-Version: 0.96.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-Edinburgh-Scanned: at nougat.ucs.ed.ac.uk with MIMEDefang 2.60, Sophie, Sophos Anti-Virus, Clam AntiVirus X-Scanned-By: MIMEDefang 2.60 on 129.215.13.205 X-Scanned-By: MIMEDefang 2.52 on 129.215.149.64 Content-Disposition: inline X-Spam: no; 0.00; co-located:01 intersection:01 algebra:01 christophe:01 dominik:01 thorsten:01 dfki:01 delahaye:01 sheard:01 soloviev:01 lucas:98 dixon:98 cartier:98 lema:98 lucas:98 [Apologies for possible multiple postings.] ------------------------------------------------------------------- CALL FOR PARTICIPATION ------------------------------------------------------------------- In co-operation with ACM SIGSAM, the International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS 2010) 8th of July 2010 Co-located with Conferences in Intelligent Computer Mathematics (CICM), including Calculemus, AISC and MKM; at CNAM, Paris. ------------------------------------------------------------------- The scope of the workshop is the intersection of programming languages and mechanized mathematics systems. This includes programming languages and aspects of present-day computer algebra systems, interactive proof assistants, and automated theorem provers, all heading towards fully integrated mechanized mathematical assistants. Registration for PLMMS and other CICM events is now open: http://cicm2010.cnam.fr/registration.html (PLMMS is on the 8th July 2010) Invited Speakers ================ Mechanized Mathematics -- Jacques Carette Beluga: programming with contextual data, contexts, and ... -- Brigitte Pientka The Abella Interactive Theorem Prover -- Andrew Gacek Can we make Mathematics universal as well as fully reliable? -- Pierre Cartier Contributed Talks ================= CTP-based program languages? Considerations about an experimental design -- Walther Neuper, Cezary Kaliszyk and Florian Haftmann Isabelle/ML vs. Isabelle/Scala -- Makarius Wenzel transalpyne: a language for automatic transposition -- Luca De Feo and Eric Schost LEMA: Towards a language for reliable arithmetic -- Vincent Lefèvre, Philippe Théveny, Florent de Dinechin, Claude-Pierre Jeannerod, Christophe Mouilleron, David Pfannholzer, Nathalie Revol The PIDE project -- Burkhart Wolff Recent Developments in Omega's Proof Search Programming Language -- Serge Autexier and Dominik Dietrich Program Committee ================= * Thorsten Altenkirch (University of Nottingham, UK) * Serge Autexier (DFKI, Germany) * David Delahaye (CNAM, Paris, France) * James Davenport [PC co-chair] (University of Bath, UK) * Lucas Dixon [PC co-chair] (University of Edinburgh, UK) * Gudmund Grov (University of Edinburgh, UK) * Ewen Maclean (University of Herriot Watt, UK) * Dale Miller (INRIA, France) * Gabriel Dos Reis (Texas A&M University, USA) * Carsten Schuermann (IT University of Copenhagen, Denmark) * Tim Sheard (Portland State University, USA) * Sergei Soloviev (IRIT, Toulouse, France) * Stephen Watt (The University of Western Ontario, Canada) * Makarius Wenzel (ITU Munich, Germany) * Freek Wiedijk (Radboud University Nijmegen, Netherlands) Links ===== * http://dream.inf.ed.ac.uk/events/plmms-2010/ the PLMMS 2010 web site * http://cicm2010.cnam.fr/ the CICM 2010 conference web site -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.