From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 1518ABC57 for ; Sat, 12 Jun 2010 13:28:22 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArICAOILE0yjrYAinGdsb2JhbACfAxUBAQEBAQgLCAkRIr4igl6COgQ X-IronPort-AV: E=Sophos;i="4.53,408,1272837600"; d="scan'208";a="52245327" Received: from incoming2.cnam.fr ([163.173.128.34]) by mail3-smtp-sop.national.inria.fr with ESMTP; 12 Jun 2010 13:28:21 +0200 From: david.delahaye@cnam.fr X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ApsEAMYJE0yjrYAN/2dsb2JhbACfdL4Ugl6COgQ X-IronPort-AV: E=Sophos;i="4.53,408,1272837600"; d="scan'208";a="15580203" Received: from urien.cnam.fr (HELO webmail.cnam.fr) ([163.173.128.13]) by outgoing2.cnam.fr with ESMTP; 12 Jun 2010 13:28:20 +0200 Received: from 87.231.49.143 (SquirrelMail authenticated user delahayd) by webmail.cnam.fr with HTTP; Sat, 12 Jun 2010 13:28:20 +0200 (CEST) Message-ID: <59597.87.231.49.143.1276342100.squirrel@webmail.cnam.fr> Date: Sat, 12 Jun 2010 13:28:20 +0200 (CEST) Subject: Calculemus 2010: Call for Participation To: caml-list@inria.fr User-Agent: SquirrelMail/1.4.13 MIME-Version: 1.0 Content-Type: text/plain;charset=iso-8859-1 Content-Transfer-Encoding: 8bit X-Priority: 3 (Normal) Importance: Normal X-Spam: no; 0.00; delahaye:01 algebra:01 algebra:01 quantifier:01 coq:01 matrices:01 markus:01 darmstadt:01 eindhoven:01 coquand:01 delahaye:01 saclay:01 renaud:01 lucas:98 dixon:98 [Apologies for cross-postings.] ------------------------------------------ CALCULEMUS 2010 - Call for Participation ------------------------------------------ 17th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning CNAM, Paris, France, July 6-7, 2010 http://cicm2010.cnam.fr/calculemus/ ******************************************* >>>> Registration is now open! <<<< (via CICM registration) http://cicm2010.cnam.fr/registration.html Registration deadline: July 4, 2010 ******************************************* Calculemus is a series of conferences dedicated to the integration of computer algebra systems (CAS) and systems for mechanised reasoning, the interactive theorem provers or proof assistants (PA) and the automated theorem provers (ATP). Currently, symbolic computation is divided into several (more or less) independent branches: traditional ones (e.g., computer algebra and mechanised reasoning) as well as newly emerging ones (on user interfaces, knowledge management, theory exploration, etc.) The main concern of the Calculemus community is to bring these developments together in order to facilitate the theory, design, and implementation of integrated systems for computer mathematics that will routinely be used by mathematicians, computer scientists and engineers in their every day business. Calculemus 2010 will be held jointly with AISC 2010 and MKM 2010 (confederated in the Conferences on Intelligent Computer Mathematics, CICM 2010) in Paris (France). Topics of Interest ================== The scope of Calculemus covers all aspects of the interplay of mechanised reasoning and computer algebra, including cross-fertilisation between those two research areas, as well as the development of integrated systems that transcend both computer algebra and theorem proving. Potential topics of interest include: * Theorem proving in computer algebra (CAS) * Computer algebra in theorem proving (PA and ATP) * Case studies and applications that both involve computer algebra and mechanised reasoning * Representation of mathematics in computer algebra * Adding computational capabilities to PA and ATP * Formal methods requiring mixed computing and proving * Combining methods of symbolic computation and formal deduction * Mathematical computation in PA and ATP * Theory, design and implementation of interdisciplinary systems for computer mathematics * Infrastructure for mathematical services * Theory exploration techniques Accepted Papers =============== This year, 7 full papers have been accepted for presentation at the conference. These papers are the following: * Formal Proof of SCHUR Conjugate Function Franck Butelle, Florent Hivert, Micaela Mayero and Frédéric Toumazet * Symbolic Domain Decomposition Jacques Carette, Alan Sexton, Volker Sorge and Stephen Watt * A Formal Quantifier Elimination for Algebraically Closed Fields Cyril Cohen and Assia Mahboubi * Computing in Coq with Infinite Algebraic Data Structures Cesar Dominguez and Julio Rubio * Formally Verified Conditions for Regularity of Interval Matrices Ioana Pasca * Reducing Expression Size using Rule-Based Integration Albert Rich and David Jeffrey * A Unified Formal Description of Arithmetic and Set Theoretical Data Types Paul Tarau In addition, there will be short presentations for extended abstracts on emerging trends, and possibly, sessions dedicated to demos. Invited Speakers ================ Andrea Asperti (University of Bologna, Italy) Jacques Carette (McMaster University, Canada) Proceedings =========== The proceedings of full papers of the conference will be published as a volume in the series Lecture Notes in Artificial Intelligence (LNAI) by Springer-Verlag. In addition to the formal proceedings published by Springer, we will provide links to online versions of the published papers from the conference website. Extended abstracts on emerging trends will be published as a technical report of CEDRIC (CNAM/ENSIIE) and will be electronically available. These papers are expected to be describing work in progress. Important Dates =============== The registration deadline is July 4, 2010. The Calculemus conference is on July 6-7, 2010. Programme Committee =================== Markus Aderhold (TU Darmstadt, Germany) Arjeh Cohen (Eindhoven University of Technology, The Netherlands) Thierry Coquand (Chalmers University of Technology, Sweden) James H. Davenport (University of Bath, UK) David Delahaye (CNAM, France), Chair Lucas Dixon (University of Edinburgh, UK) William M. Farmer (McMaster University, Canada) Temur Kutsia (RISC, Austria) Assia Mahboubi (INRIA Saclay, France) Renaud Rioboo (ENSIIE, France), Chair Julio Rubio (Universidad de La Rioja, Spain) Volker Sorge (University of Birmingham, UK) Stephen M. Watt (University of Western Ontario, Canada) Freek Wiedijk (Radboud University Nijmegen, The Netherlands) Wolfgang Windsteiger (RISC, Austria)