Screenshot instructions:
Windows
Mac
Red Hat Linux
Ubuntu
Click URL instructions:
Rightclick on ad, choose "Copy Link", then paste here →
(This may not be possible with some types of ads)
You can subscribe to this list here.
2007 
_{Jan}

_{Feb}

_{Mar}

_{Apr}

_{May}

_{Jun}

_{Jul}

_{Aug}
(2) 
_{Sep}
(1) 
_{Oct}

_{Nov}

_{Dec}


2008 
_{Jan}

_{Feb}
(1) 
_{Mar}

_{Apr}

_{May}

_{Jun}

_{Jul}

_{Aug}
(1) 
_{Sep}

_{Oct}
(1) 
_{Nov}

_{Dec}
(2) 
2009 
_{Jan}
(2) 
_{Feb}
(3) 
_{Mar}
(1) 
_{Apr}
(3) 
_{May}

_{Jun}

_{Jul}

_{Aug}
(1) 
_{Sep}

_{Oct}

_{Nov}

_{Dec}

2010 
_{Jan}
(4) 
_{Feb}

_{Mar}
(3) 
_{Apr}

_{May}

_{Jun}
(1) 
_{Jul}
(1) 
_{Aug}

_{Sep}

_{Oct}

_{Nov}

_{Dec}

2011 
_{Jan}

_{Feb}

_{Mar}

_{Apr}

_{May}

_{Jun}

_{Jul}
(1) 
_{Aug}

_{Sep}
(1) 
_{Oct}

_{Nov}

_{Dec}

2012 
_{Jan}
(1) 
_{Feb}
(1) 
_{Mar}

_{Apr}

_{May}

_{Jun}

_{Jul}

_{Aug}

_{Sep}

_{Oct}

_{Nov}

_{Dec}

2013 
_{Jan}

_{Feb}

_{Mar}
(1) 
_{Apr}

_{May}
(1) 
_{Jun}

_{Jul}

_{Aug}

_{Sep}

_{Oct}

_{Nov}

_{Dec}

From: SYNASC 2013 <synasc13@sy...>  20130512 18:10:27

[Please post  apologies for multiple copies.] Call for Papers  SYNASC 2013 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing September 2326, 2013, Timisoara, Romania http://www.synasc.ro/ Aim  SYNASC aims to stimulate the interaction between the two scientific communities of symbolic and numeric computing and to exhibit interesting applications of the areas both in theory and in practice. The choice of the topic is motivated by the belief of the organizers that the dialogue between the two communities is very necessary for accelerating the progress in making the computer a truly intelligent aid for mathematicians and engineers. Important Dates  19 May 2013 : Abstract submission 26 May 2013 : Paper submission 22 July 2013 : Notification of acceptance 01 September 2013 : Registration 08 September 2013 : Revised papers according to the reviews 2326 September 2013 : Symposium 30 November 2013 : Final papers for postproceedings Tracks  * Symbolic Computation + computer algebra + symbolic techniques applied to numerics + hybrid symbolic and numeric algorithms + numerics and symbolics for geometry + programming with constraints, narrowing * Logic and Programming + automatic reasoning + formal system verification + formal verification and synthesis + software quality assessment + static analysis + timing analysis * Artificial Intelligence + methods for hard computational problems + intelligent systems for scientific computing + agentbased complex systems modeling and development + scientific knowledge management + computational intelligence + machine learning + recommender and expert systems for scientific computing + data mining and web mining + natural language processing + uncertain reasoning in scientific computing + intelligent hybrid systems * Numerical Computing + iterative approximation of fixed points + solving systems of nonlinear equations + numerical and symbolic algorithms for differential equations + numerical and symbolic algorithms for optimization + parallel algorithms for numerical computing + scientific visualization and image processing * Distributed Computing + parallel and distributed algorithms for clouds, GPUs, HPC, P2P systems, autonomous systems. Work should focus on scheduling, scaling, load balancing, networks, faulttolerance, gossip algorithms, energy saving + applications for parallel and distributed systems, including work on cross disciplinary (scientific) applications for grids/clouds, web applications, workflow platforms, network measurement tools, programming environments + architectures for parallel and distributed systems, including selfmanaging and autonomous systems, negotiation protocols, HPC on clouds, GPU processing, PaaS for (inter)cloud, brokering platforms, mobile computing + modelling of parallel and distributed systems including models on resources and networks, semantic representation, negotiation, social networks, trace management, simulators + any other topic deemed relevant to the field * Advances in the Theory of Computing + Data structures and algorithms + Combinatorial Optimization + Formal languages and Combinatorics on Words + Graphtheoretic and Combinatorial methods in Computer Science + Algorithmic paradigms, including distributed, online, approximation, probabilistic, gametheoretic algorithms + Computational Complexity Theory, including structural complexity, boolean complexity, communication complexity, averagecase complexity, derandomization and property testing + Logical approaches to complexity, including finite model theory + Algorithmic and computational learning theory + Aspects of computability theory, including computability in analysis and algorithmic information theory + Proof complexity + Computational social choice and game theory + New computational paradigms: CNN computing, quantum, holographic and other nonstandard approaches to Computability + Randomized methods, random graphs, threshold phenomena and typicalcase complexity + Automata theory and other formal models, particularly in relation to formal verification methods such as model checking and runtime verification + Applications of theory, including wireless and sensor networks, computational biology and computational economics + Experimental algorithmics Workshops  * Workshop on Agents for Complex Systems (ACSys) http://www.synasc.ro/workshops/acsys2013/ * Workshop of HPC for scientific problems (HPCS) http://host.hpc.uvt.ro/events/hpcs/ * Workshop on Iterative Approximation of Fixed Points (IAFP) http://www.synasc.ro/workshops/iafp2013/ * Workshop on Management of Resources and Services in Cloud and Sky Computing (MICAS) http://amicas.hpc.uvt.ro/micas2013/ * Workshop on Natural Computing and Applications (NCA) http://www.synasc.ro/workshops/nca2013/ Workshops deadlines: please visit each workshop webpage Tutorials  * Tutorial HPC http://host.hpc.uvt.ro/hpcs#HPCTutorial * Tutorial MultiCloud http://amicas.hpc.uvt.ro/micas2013#MultiCloudTutorial Publication  Research papers that are accepted and presented at the symposium will be collected as postproceedings published by Conference Publishing Service (CPS) (indexed in ISI Web of Science, DBLP, SCOPUS). Invited Speakers  * Ivona Brandic, Vienna University of Technology, Austria * Gabriel Ciobanu, Romanian Academy, Institute of Computer Science, Iasi, Romania * Leonardo de Moura, Microsoft Research, USA * Grigore Rosu, University of Illinois at UrbanaChampaign, USA * Dan A. Simovici, University of Massachusetts Boston, USA Honorary Chairs  * Bruno Buchberger, Johannes Kepler University, Austria * Stefan Maruster, West University of Timisoara, Romania Steering Committee  * Tetsuo Ida, University of Tsukuba, Japan * Tudor Jebelean, Johannes Kepler University, Austria * Viorel Negru, West University of Timisoara, Romania * Dana Petcu, West University of Timisoara, Romania * Stephen Watt, University of Western Ontario, Canada * Daniela Zaharie, West University of Timisoara, Romania General Chair  * Viorel Negru, West University of Timisoara, Romania Program Chair  * Nikolaj Bjorner, Microsoft Research, US Track Chairs  * Symbolic Computation + Tetsuo Ida, University of Tsukuba, Japan + Stephen Watt, University of Western Ontario, Canada * Logic and Programming + Tudor Jebelean, Johannes Kepler University, Austria + Laura Kovacs, Vienna University of Technology, Austria * Artificial Intelligence + Andrei Petrovski, Robert Gordon University, UK + Daniela Zaharie, West University of Timisoara, Romania * Numerical Computing + Yonghong Yao, Tianjin Polytechnic University, China + Ioan A. Rus, "BabesBolyai" University of ClujNapoca, Romania * Distributed Computing + Marc Frincu, West University of Timisoara, Romania + Karoly Bosa, Johannes Kepler University, Austria * Advances in the Theory of Computing + Mircea Marin, West University of Timisoara, Romania + Gabriel Istrate, Research Institute eAustria Timisoara, Romania Special sessions and workshops chair  * Dana Petcu, West University of Timisoara, Romania Tutorial chair  * Adrian Craciun, West University of Timisoara, Romania Proceedings Chairs  * Nikolaj Bjorner, Microsoft Research, US * Daniela Zaharie, West University of Timisoara, Romania Local Committee Chairs  * Isabela Dramnesc, West University of Timisoara, Romania * Silviu Panica, Institute eAustria Timisoara, Romania Submission  Submissions of research papers are invited. The papers must contain original research results not submitted and not published elsewhere. The submission process consists of two steps. * In the first step the authors are invited to express their intention to participate at the conference by submitting a short abstract (1/2 page, at maximum) where it is clearly stated the main contribution(s) of the paper. * In the second step the authors should submit the full paper (up to 8 pages in the twocolumns IEEE conference style). Both the abstract and the full paper should be submitted electronically through http://www.easychair.org/conferences/?conf=synasc2013 (for the main tracks) and through http://www.easychair.org/conferences/?conf=synasc2013workshops (for the workshops). Proposals are also invited for: * special sessions Special sessions  Proposals are invited for special sessions on any topic relevant to the conference. Special sessions are intended to stimulate indepth discussions in special areas and they are fully integrated into the main conference. The research papers and the informal presentations submitted and accepted for the special sessions follow the same rules as the papers submitted to the regular sessions. It is expected that the organizers of the special sessions appoint their own chair and program committee, which will be integrated in the conference program committee and will be supervised by the conference programme chair and by the general chair.  SYNASC 2013 West University of Timisoara Department of Computer Science Bd. V. Parvan 4, 300223 Timisoara, Romania tel: + (40) 256 592155, +(40) 256 592195 fax: + (40) 256 592316, +(40) 256 592380 email: synasc13@... 
From: Gabriel Dos Reis <gdr@in...>  20130302 13:06:11

FYI.  Forwarded message  From: Jérémy FIDELAK <jeremy.fidelak@...> Date: Fri, Feb 22, 2013 at 7:11 AM Subject: Inria : Manuel Bronstein's codes / Open source diffusion To: openaxiomdevelowner@... Dear Sir, I would like to announce that Manuel Bronstein's codes are published under open source license (see message below). Could you diffuse this information on openaxiomdevel list ? thank you in advance JFIDELAK  Dear all, I am pleased to inform you that Inria decided to publish Manuel Bronstein's codes under the CeCILL open source license. Dr. Manuel Bronstein was the leader of InriaCAFE project team and was a prominent scientist in computer algebra and mathematics. He died of heart attack on june 6, 2005. These codes are hosted here : https://gforge.inria.fr/projects/bronsteincodes/ You can freely use them while complying with the terms of the CeCILL license (GPL compatible). Best regards,  Jérémy FIDELAK, Ph.D. Partnerships & Technology Transfer Officer Inria Sophia AntipolisMéditerranée Research Center 2004, route des Lucioles  BP 93 F  06902 Sophia Antipolis cedex Phone : +33 4 92 38 76 49 Web : http://www.inria.fr/sophia 
From: Gabriel Dos Reis <gdr@cs...>  20120218 01:38:47

CICM 2012  Conference on Intelligent Computer Mathematics July 913, 2012 at Jacobs University, Bremen, Germany http://www.informatik.unibremen.de/cicm2012/ Call for Papers  As computers and communications technology advance, greater opportunities arise for intelligent mathematical computation. While computer algebra, automated deduction, mathematical publishing and novel user interfaces individually have long and successful histories, we are now seeing increasing opportunities for synergy among these areas. The Conference on Intelligent Computer Mathematics offers a venue for discussing these areas and their synergy. The conference will be organized by Serge Autexier and Michael Kohlhase at Jacobs University in Bremen and consist of five tracks: Artificial Intelligence and Symbolic Computation (AISC) CoChairs: John A. Campbell, Jacques Carette Calculemus Chair: Gabriel Dos Reis Digital Mathematical Libraries (DML) Chair: Petr Sojka Mathematical Knowledge Management (MKM) Chair: Makarius Wenzel Systems and Projects Chair: Volker Sorge The overall programme will be organized by the General Program Chair Johan Jeuring. Invited talks will be given by: Yannis Haralambous, Département Informatique, Télécom Bretagne Conor McBride, Department of Computer and Information Sciences, University of Strathclyde Cezar Ionescu, Potsdam Institute for Climate Impact Research  Important dates  Abstract submission: 20 February 2012 Submission deadline: 26 February 2012 Reviews sent to authors: 23 March 2012 Rebuttals due: 30 March 2012 Notification of acceptance: 6 April 2012 Camera ready copies due: 20 April 2012 Conference: 913 July 2012  Tracks  *** AISC *** Symbolic computation can be roughly described as the study of algorithms which operate on expression trees. Another way to phrase this is to say that the denotational semantics of expressions trees is not fixed, but is rather context dependent. Expression simplification is probably the archetypal symbolic computation. Mathematically oriented software (such as the socalled computer algebra systems) have been doing this for decades, but not long thereafter, systems doing proof planning and theorem discovery also started doing the same; some attempts at knowledge management and 'expert systems' were also symbolic, but less successfully so. More recently, many different kinds of program analyses have gotten `symbolic', as well as some of the automated theorem proving (SMT, CAV, etc). But a large number of the underlying problems solved by symbolic techniques are well known to be undecidable (never mind the many that are EXPtime complete, etc). Artificial Intelligence has been attacking many of these different subproblems for quite some time, and has also built up a solid body of knowledge. In fact, most symbolic computation systems grew out of AI projects. These two fields definitely intersect. One could say that in the intersection lies all those problems for which we have no decision procedures. In other words, decision procedures mark a definite phase shift in our understanding, but are not always possible. Yet we still want to solve certain problems, and must find 'other' means of (partial) solution. This is the fertile land which comprises the core of AISC. Rather than try to exhaustively list topics of interest, it is simplest to say that AISC seeks work which advances the understanding of Solving problems which fundamentally involve the manipulation of expressions, but for which decision procedures are unlikely to ever exist. *** Calculemus *** 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. The topics of interest of Calculemus include but are not limited to: * 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 * Theory exploration techniques * Input languages, programming languages, types and constraint languages, and modeling languages for mechanised mathematics systems (PA, CAS, and ATP). * Infrastructure for mathematical services *** DML *** Mathematicians dream of a digital archive containing all peerreviewed mathematical literature ever published, properly linked, validated and verified. It is estimated that the entire corpus of mathematical knowledge published over the centuries does not exceed 100,000,000 pages, an amount easily manageable by current information technologies. Following success of DML 2008, DML 2009 DML 2010, and DML 2011 track objectives are to formulate the strategy and goals of a global mathematical digital library and to summarize the current successes and failures of ongoing technologies and related projects as EuDML, asking such questions as: * What technologies, standards, algorithms and formats should be used and what metadata should be shared? * What business models are suitable for publishers of mathematical literature, authors and funders of their projects and institutions? * Is there a model of sustainable, interoperable, and extensible mathematical library that mathematicians can use in their everyday work? * What is the best practice for * retrodigitized mathematics (from images via OCR to MathML or TeX); * retroborndigital mathematics (from existing electronic copy in DVI, PS or PDF to MathML or TeX); * borndigital mathematics (how to make needed metadata and file formats available as a side effect of publishing workflow [CEDRAM/Euclid model])? DML is an opportunity to share experience and best practices between projects in any area (MKM, NLP, OCR, pattern recognition, whatever) that could change the paradigm for searching, accessing, and interacting with the mathematical corpus. The track is trans/interdisciplinary and contributions from any kind of people on any aspect of the DML building are welcome. *** MKM *** Mathematical Knowledge Management is an interdisciplinary field of research in the intersection of mathematics, computer science, library science, and scientific publishing. The objective of MKM is to develop new and better ways of managing sophisticated mathematical knowledge, based on innovative technology of computer science, the Internet, and intelligent knowledge processing. MKM is expected to serve mathematicians, scientists, and engineers who produce and use mathematical knowledge; educators and students who teach and learn mathematics; publishers who offer mathematical textbooks and disseminate new mathematical results; and librarians and mathematicians who catalog and organize mathematical knowledge. The conference is concerned with all aspects of mathematical knowledge management. A nonexclusive list of important topics includes: * Representations of mathematical knowledge * Authoring languages and tools * Repositories of formalized mathematics * Deduction systems * Mathematical digital libraries * Diagrammatic representations * Mathematical OCR * Mathematical search and retrieval * Math assistants, tutoring and assessment systems * MathML, OpenMath, and other mathematical content standards * Web presentation of mathematics * Data mining, discovery, theory exploration * Computer algebra systems * Collaboration tools for mathematics * Challenges and solutions for mathematical workflows *** Systems and Projects *** The Systems and Projects track of the Conferences on Intelligent Computer Mathematics is a forum for presentation of systems and new and ongoing projects in all areas and topics related to the CICM conferences: * AI and Symbolic Computation * Deduction and Computer Algebra * Mathematical Knowledge Management * Digital Mathematical Libraries The track aims to provide an overview of the latest developments and trends within the CICM community as well as to exchange ideas between developers and introduce systems to an audience of potential users. We solicit submissions for two page abstracts in the categories of system descriptions and project presentations. System description should present * newly developed systems, * systems that have not previously been presented to the CICM community, or * significant updates to existing systems. Project presentation should describe * projects that are new or about to start, * ongoing projects that have not yet been presented to the CICM community. * significant new developments in ongoing previously presented projects. All submissions should contain links to demos, downloadable systems, or project pages. Availability of such accompanying material will be a strong prerequisite for acceptance. Accepted abstracts will be published in the CICM proceedings in Springer's LNAI series. Author's are expected to present their abstracts in 510 minute teaser talks followed by an open demo/poster session. System papers must be accompanied by a system demonstration, while project papers must be accompanied by a poster presentation.  Submitting  Submissions to tracks A to D must not exceed 15 pages and will be reviewed and evaluated with respect to relevance, clarity, quality, originality, and impact. Shorter papers, e.g., for system descriptions, are welcome. Authors will have an opportunity to respond to their papers' reviews before the programme committee makes a decision. Submissions to the Systems & Projects track must not exceed four pages. The accepted abstracts will be presented at CICM in a fast presentation session, followed by an open demo/poster session. System papers must be accompanied by a system demonstration, and project papers must be accompanied by a poster presentation. The four pages of the abstract should be new material, accompanied by links to demos/downloads/projectpages and [existing] system descriptions. Availability of such accompanying material will be a strong prerequisite for acceptance. Accepted conference submissions from all tracks will be published as a volume in the series Lecture Notes in Artificial Intelligence (LNAI) by Springer. In addition to these formal proceedings, authors are permitted and encouraged to publish the final versions of their papers on arXiv.org. Workinprogress submissions are intended to provide a forum for the presentation of original work that is not (yet) in a suitable form for submission as a full or system description paper. This includes work in progress and emerging trends. Their size is not limited, but we recommend 5  10 pages. The programme committee may offer authors of rejected formal submissions to publish their contributions as workinprogress papers instead. Depending on the number of workinprogress papers accepted, they will be presented at the conference either as short talks or as posters. The workinprogress proceedings will be published as a technical report. All papers should be prepared in LaTeX and formatted according to the requirements of Springer's LNCS series (the corresponding style files can be downloaded from http://www.springer.de/comp/lncs/authors.html). By submitting a paper the authors agree that if it is accepted at least one of the authors will attend the conference to present it. Electronic submission is done through easychair (http://www.easychair.org/conferences/?conf=cicm2012).  Program Committees  General chair: Johan Jeuring (Utrecht University and Open Universiteit the Netherlands) AISC track John A. Campbell; University College London, UK; Cochair Jacques Carette; McMaster University, Canada; Cochair Serge Autexier; DFKI Bremen, Germany Jacques Calmet; University of Karlsruhe, Germany Jacques Fleuriot; University of Edinburgh, UK Andrea Kohlhase; International University Bremen, Germany Erik Postma; Maplesoft Inc., Canada Alan Sexton; University of Birmingham, UK Chungchieh Shan; Cornell University, USA. Stephen Watt; University of Western Ontario, Canada Calculemus track Gabriel Dos Reis; Texas A&M University, USA; Chair Andrea Asperti; University of Bologna, Italy Laurent Bernardin; Maplesoft, Canada James Davenport; University of Bath, UK Ruben Gamboa; University of Wyoming, USA Mark Giesbrecht; University of Waterloo, Canada Sumit Gulwani; Microsoft Research, USA John Harrison; Intel, USA Joris van der Hoeven; École Polytechnique, France Hoon Hong; North Carolina State University, USA Loïc Pottier; INRIA, France Wolfgang Windsteiger; RISC, Austria DML track Petr Sojka; Masaryk University, Brno, CZ; Chair José Borbinha; Technical University of Lisbon, PT Thierry Bouche; University Grenoble, FR Michael Doob; University of Manitoba, Winnipeg, CA Thomas Fischer; Goettingen University, DE Yannis Haralambous; Télécom Bretagne, FR Václav Hlaváč; Czech Technical University, Prague, CZ Michael Kohlhase; Jacobs University Bremen, DE Janka Chlebíková; Portsmouth University, UK Enrique MaciásVirgós; University of Santiago de Compostela, ES Bruce Miller; NIST, USA Jiří Rákosník; Academy of Sciences, Prague, CZ Eugenio Rocha; University of Aveiro, PT David Ruddy; Cornell University, US Volker Sorge; University of Birmingham, UK Masakazu Suzuki; Kyushu University, JP MKM track Makarius Wenzel; University of ParisSouth, France; Chair David Aspinall; University of Edinburgh, Scotland Jeremy Avigad; Carnegie Mellon University, USA Mateja Jamnik; University of Cambridge, UK Cezary Kaliszyk; University of Tsukuba, Japan Manfred Kerber; University of Birmingham, UK Christoph Lüth; DFKI Bremen, Germany Adam Naumowicz; University of Białystok, Poland Jim Pitman; University of California, Berkeley, USA Pedro Quaresma; Universidade de Coimbra, Portugal Florian Rabe; Jacobs University Bremen, Germany Claudio Sacerdoti Coen; University of Bologna, Italy Enrico Tassi; INRIA Saclay, France Freek Wiedijk; Radboud University Nijmegen, The Netherlands Systems & Projects track Volker Sorge; University of Birmingham, UK; Chair Josef Baker; University of Birmingham, UK John Charnley; Imperial College, UK Manuel Kauers; RISC, Austria Koji Nakagawa; Kyushu University, Japan Piotr Rudnicki; University of Alberta, Canada Josef Urban; Radboud University Nijmegen, The Netherlands Richard Zanibbi; Rochester Institute of Technologies, USA 
From: Gabriel Dos Reis <gdr@cs...>  20120109 13:13:08

Apologies for duplicate copies. CICM 2012  Conference on Intelligent Computer Mathematics July 913, 2012 at Jacobs University, Bremen, Germany http://www.informatik.unibremen.de/cicm2012/ Call for Papers  As computers and communications technology advance, greater opportunities arise for intelligent mathematical computation. While computer algebra, automated deduction, mathematical publishing and novel user interfaces individually have long and successful histories, we are now seeing increasing opportunities for synergy among these areas. The Conference on Intelligent Computer Mathematics offers a venue for discussing these areas and their synergy. The conference will be organized by Serge Autexier and Michael Kohlhase at Jacobs University in Bremen and consist of five tracks: Artificial Intelligence and Symbolic Computation (AISC) CoChairs: John A. Campbell, Jacques Carette Calculemus Chair: Gabriel Dos Reis Digital Mathematical Libraries (DML) Chair: Petr Sojka Mathematical Knowledge Management (MKM) Chair: Makarius Wenzel Systems and Projects Chair: Volker Sorge The overall programme will be organized by the General Program Chair Johan Jeuring. Invited talks will be given by: Yannis Haralambous, Département Informatique, Télécom Bretagne Conor McBride, Department of Computer and Information Sciences, University of Strathclyde Cezar Ionescu, Potsdam Institute for Climate Impact Research  Important dates  Abstract submission: 20 February 2012 Submission deadline: 26 February 2012 Reviews sent to authors: 23 March 2012 Rebuttals due: 30 March 2012 Notification of acceptance: 6 April 2012 Camera ready copies due: 20 April 2012 Conference: 913 July 2012  Tracks  *** AISC *** Symbolic computation can be roughly described as the study of algorithms which operate on expression trees. Another way to phrase this is to say that the denotational semantics of expressions trees is not fixed, but is rather context dependent. Expression simplification is probably the archetypal symbolic computation. Mathematically oriented software (such as the socalled computer algebra systems) have been doing this for decades, but not long thereafter, systems doing proof planning and theorem discovery also started doing the same; some attempts at knowledge management and 'expert systems' were also symbolic, but less successfully so. More recently, many different kinds of program analyses have gotten `symbolic', as well as some of the automated theorem proving (SMT, CAV, etc). But a large number of the underlying problems solved by symbolic techniques are well known to be undecidable (never mind the many that are EXPtime complete, etc). Artificial Intelligence has been attacking many of these different subproblems for quite some time, and has also built up a solid body of knowledge. In fact, most symbolic computation systems grew out of AI projects. These two fields definitely intersect. One could say that in the intersection lies all those problems for which we have no decision procedures. In other words, decision procedures mark a definite phase shift in our understanding, but are not always possible. Yet we still want to solve certain problems, and must find 'other' means of (partial) solution. This is the fertile land which comprises the core of AISC. Rather than try to exhaustively list topics of interest, it is simplest to say that AISC seeks work which advances the understanding of Solving problems which fundamentally involve the manipulation of expressions, but for which decision procedures are unlikely to ever exist. *** Calculemus *** 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. The topics of interest of Calculemus include but are not limited to: * 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 * Theory exploration techniques * Input languages, programming languages, types and constraint languages, and modeling languages for mechanised mathematics systems (PA, CAS, and ATP). * Infrastructure for mathematical services *** DML *** Mathematicians dream of a digital archive containing all peerreviewed mathematical literature ever published, properly linked, validated and verified. It is estimated that the entire corpus of mathematical knowledge published over the centuries does not exceed 100,000,000 pages, an amount easily manageable by current information technologies. Following success of DML 2008, DML 2009 DML 2010, and DML 2011 track objectives are to formulate the strategy and goals of a global mathematical digital library and to summarize the current successes and failures of ongoing technologies and related projects as EuDML, asking such questions as: * What technologies, standards, algorithms and formats should be used and what metadata should be shared? * What business models are suitable for publishers of mathematical literature, authors and funders of their projects and institutions? * Is there a model of sustainable, interoperable, and extensible mathematical library that mathematicians can use in their everyday work? * What is the best practice for * retrodigitized mathematics (from images via OCR to MathML or TeX); * retroborndigital mathematics (from existing electronic copy in DVI, PS or PDF to MathML or TeX); * borndigital mathematics (how to make needed metadata and file formats available as a side effect of publishing workflow [CEDRAM/Euclid model])? DML is an opportunity to share experience and best practices between projects in any area (MKM, NLP, OCR, pattern recognition, whatever) that could change the paradigm for searching, accessing, and interacting with the mathematical corpus. The track is trans/interdisciplinary and contributions from any kind of people on any aspect of the DML building are welcome. *** MKM *** Mathematical Knowledge Management is an interdisciplinary field of research in the intersection of mathematics, computer science, library science, and scientific publishing. The objective of MKM is to develop new and better ways of managing sophisticated mathematical knowledge, based on innovative technology of computer science, the Internet, and intelligent knowledge processing. MKM is expected to serve mathematicians, scientists, and engineers who produce and use mathematical knowledge; educators and students who teach and learn mathematics; publishers who offer mathematical textbooks and disseminate new mathematical results; and librarians and mathematicians who catalog and organize mathematical knowledge. The conference is concerned with all aspects of mathematical knowledge management. A nonexclusive list of important topics includes: * Representations of mathematical knowledge * Authoring languages and tools * Repositories of formalized mathematics * Deduction systems * Mathematical digital libraries * Diagrammatic representations * Mathematical OCR * Mathematical search and retrieval * Math assistants, tutoring and assessment systems * MathML, OpenMath, and other mathematical content standards * Web presentation of mathematics * Data mining, discovery, theory exploration * Computer algebra systems * Collaboration tools for mathematics * Challenges and solutions for mathematical workflows *** Systems and Projects *** The Systems and Projects track of the Conferences on Intelligent Computer Mathematics is a forum for presentation of systems and new and ongoing projects in all areas and topics related to the CICM conferences: * AI and Symbolic Computation * Deduction and Computer Algebra * Mathematical Knowledge Management * Digital Mathematical Libraries The track aims to provide an overview of the latest developments and trends within the CICM community as well as to exchange ideas between developers and introduce systems to an audience of potential users. We solicit submissions for two page abstracts in the categories of system descriptions and project presentations. System description should present * newly developed systems, * systems that have not previously been presented to the CICM community, or * significant updates to existing systems. Project presentation should describe * projects that are new or about to start, * ongoing projects that have not yet been presented to the CICM community. * significant new developments in ongoing previously presented projects. All submissions should contain links to demos, downloadable systems, or project pages. Availability of such accompanying material will be a strong prerequisite for acceptance. Accepted abstracts will be published in the CICM proceedings in Springer's LNAI series. Author's are expected to present their abstracts in 510 minute teaser talks followed by an open demo/poster session. System papers must be accompanied by a system demonstration, while project papers must be accompanied by a poster presentation.  Submitting  Submissions to tracks A to D must not exceed 15 pages and will be reviewed and evaluated with respect to relevance, clarity, quality, originality, and impact. Shorter papers, e.g., for system descriptions, are welcome. Authors will have an opportunity to respond to their papers' reviews before the programme committee makes a decision. Submissions to the Systems & Projects track must not exceed four pages. The accepted abstracts will be presented at CICM in a fast presentation session, followed by an open demo/poster session. System papers must be accompanied by a system demonstration, and project papers must be accompanied by a poster presentation. The four pages of the abstract should be new material, accompanied by links to demos/downloads/projectpages and [existing] system descriptions. Availability of such accompanying material will be a strong prerequisite for acceptance. Accepted conference submissions from all tracks will be published as a volume in the series Lecture Notes in Artificial Intelligence (LNAI) by Springer. In addition to these formal proceedings, authors are permitted and encouraged to publish the final versions of their papers on arXiv.org. Workinprogress submissions are intended to provide a forum for the presentation of original work that is not (yet) in a suitable form for submission as a full or system description paper. This includes work in progress and emerging trends. Their size is not limited, but we recommend 5  10 pages. The programme committee may offer authors of rejected formal submissions to publish their contributions as workinprogress papers instead. Depending on the number of workinprogress papers accepted, they will be presented at the conference either as short talks or as posters. The workinprogress proceedings will be published as a technical report. All papers should be prepared in LaTeX and formatted according to the requirements of Springer's LNCS series (the corresponding style files can be downloaded from http://www.springer.de/comp/lncs/authors.html). By submitting a paper the authors agree that if it is accepted at least one of the authors will attend the conference to present it. Electronic submission is done through easychair (http://www.easychair.org/conferences/?conf=cicm2012).  Program Committees  General chair: Johan Jeuring (Utrecht University and Open Universiteit the Netherlands) AISC track John A. Campbell; University College London, UK; Cochair Jacques Carette; McMaster University, Canada; Cochair Serge Autexier; DFKI Bremen, Germany Jacques Calmet; University of Karlsruhe, Germany Jacques Fleuriot; University of Edinburgh, UK Andrea Kohlhase; International University Bremen, Germany Erik Postma; Maplesoft Inc., Canada Alan Sexton; University of Birmingham, UK Chungchieh Shan; Cornell University, USA. Stephen Watt; University of Western Ontario, Canada Calculemus track Gabriel Dos Reis; Texas A&M University, USA; Chair Andrea Asperti; University of Bologna, Italy Laurent Bernardin; Maplesoft, Canada James Davenport; University of Bath, UK Ruben Gamboa; University of Wyoming, USA Mark Giesbrecht; University of Waterloo, Canada Sumit Gulwani; Microsoft Research, USA John Harrison; Intel, USA Joris van der Hoeven; École Polytechnique, France Hoon Hong; North Carolina State University, USA Loïc Pottier; INRIA, France Wolfgang Windsteiger; RISC, Austria DML track Petr Sojka; Masaryk University, Brno, CZ; Chair José Borbinha; Technical University of Lisbon, PT Thierry Bouche; University Grenoble, FR Michael Doob; University of Manitoba, Winnipeg, CA Thomas Fischer; Goettingen University, DE Yannis Haralambous; Télécom Bretagne, FR Václav Hlaváč; Czech Technical University, Prague, CZ Michael Kohlhase; Jacobs University Bremen, DE Janka Chlebíková; Portsmouth University, UK Enrique MaciásVirgós; University of Santiago de Compostela, ES Bruce Miller; NIST, USA Jiří Rákosník; Academy of Sciences, Prague, CZ Eugenio Rocha; University of Aveiro, PT David Ruddy; Cornell University, US Volker Sorge; University of Birmingham, UK Masakazu Suzuki; Kyushu University, JP MKM track Makarius Wenzel; University of ParisSouth, France; Chair David Aspinall; University of Edinburgh, Scotland Jeremy Avigad; Carnegie Mellon University, USA Mateja Jamnik; University of Cambridge, UK Cezary Kaliszyk; University of Tsukuba, Japan Manfred Kerber; University of Birmingham, UK Christoph Lüth; DFKI Bremen, Germany Adam Naumowicz; University of Białystok, Poland Jim Pitman; University of California, Berkeley, USA Pedro Quaresma; Universidade de Coimbra, Portugal Florian Rabe; Jacobs University Bremen, Germany Claudio Sacerdoti Coen; University of Bologna, Italy Enrico Tassi; INRIA Saclay, France Freek Wiedijk; Radboud University Nijmegen, The Netherlands Systems & Projects track Volker Sorge; University of Birmingham, UK; Chair Josef Baker; University of Birmingham, UK John Charnley; Imperial College, UK Manuel Kauers; RISC, Austria Koji Nakagawa; Kyushu University, Japan Piotr Rudnicki; University of Alberta, Canada Josef Urban; Radboud University Nijmegen, The Netherlands Richard Zanibbi; Rochester Institute of Technologies, USA 
From: Gabriel Dos Reis <gdr@cs...>  20110904 13:54:18

Игорь Пашев <pashev.igor@...> writes:  Merry Christmas! :)   http://packages.debian.org/sid/openaxiom Thank Igor!  Gaby 
From: Gabriel Dos Reis <gdr@cs...>  20110709 19:33:22

The following message is a courtesy copy of an article that has been posted to sci.math.symbolic as well. Hi, I'm pleased to announce that OpenAxiom1.4.1 was released on July 7, 2011. OpenAxiom is an open source platform for scientific and engineering computations, with an emphasis on symbolic, numeric, and algebraic computations. This is a bug fix release in the OpenAxiom 1.4.x series. This release adds improvements to the interpreter, the compiler, the algebra set, an the new GUI interface on Windows platforms. More information on new features can be found at http://www.openaxiom.org/1.4/ OpenAxiom1.4.1 is known to build and run on major Unix systems, GNU/Linux systems, Windows (MinGW/MSYS, mingw64), Mac OS X, and handheld devices. The source code of OpenAxiom is available for download from http://www.openaxiom.org/download.html Furthermore, precompiled binaries (Windows, Fedora, Mandriva, openSUSE) are also available for download. OpenAxiom is a free software released under a BSDtype license. For more information about OpenAxiom, please visit us at http://www.openaxiom.org/ Feel free to use our Bug Tracker https://sourceforge.net/tracker/?group_id=203172 to report issues related to uses, build, or installation of OpenAxiom, or requests for improvements. Drop us a note at openaxiomhelp@... I'm grateful to the people who helped improve this release and make it possible. In particular, Alfredo Portes and Michael Becker relentlessly helped with testing on Windows platforms. Enjoy.  Gaby 
From: Daniel de Angelis Cordeiro <Daniel.Cordeiro@im...>  20100713 13:56:43

Matrix product over multiprecision integer and gcd computation http://pasco2010.imag.fr/contest.html 21st23rd July 2010 PASCO 2010 Programming Challenge http://pasco2010.imag.fr/ Call for Participation  Since the 80s and during the 90s a lot of parallel algorithms was proposed for computer algebra. Thus, 30 years after few computer algebra system are able to exploit modern parallel architectures multicore, cluster and GPUs. The International Workshop on Parallel and Symbolic Computation (PASCO) is a series of workshops dedicated to the promotion and advancement of parallel algorithms and software in all areas of symbolic mathematical computation. The pervasive ubiquity of parallel architectures and memory hierarchy has led to the emergence of a new quest for parallel mathematical algorithms and software capable of exploiting the various levels of parallelism: from hardware acceleration technologies (multicore and multiprocessor system on chip, GPGPU, FPGA) to cluster and global computing platforms. To push up the limits of symbolic and algebraic computations, beyond the optimization of the application itself, the effective use of a large number of resources  memory and general or specialized computing units  is expected to enhance the performance multicriteria objectives: time, energy consumption, resource usage, reliability. This year the PASCO 2010 workshop organize two programming challenges on ones of the most fundamental algorithms arising in computer algebra and providing rich opportunities for high performance computing. The two problems are matrix multiplication and gcd computations. Instances of the problems are given on the web site. The competition will take place live during the PASCO 2010 workshop. The results of the competition will be presented as part of the PASCO 2010 program. All participating teams will run their program on a selected set of the problems. The rule of the game is available on the PASCO 2010 workshop site [http://pasco2010.imag.fr/contest.html]. We strongly encourage all developers of parallel program or developers of parallel computer algebra system tools to participate in the competition. Teams are invited to send a declaration of participation as soon as possible by sending a mail to the PASCO 2010 conference organizers at pasco2010@... with the following information: * The name of the team and the contact information (name, email address, institution or company) of each team member willing to participate to the PASCO 2010 programming contest; * The name of the contact person (interlocutor and team representative). Accounts will be created on machine to allow teams to prepare their competition. Important dates  Team declaration of participation: 19 July 2010 Preparation of the team: From 18 June until 20 July (remotely) Final preparation day: Wednesday 21 July 2010 at the Conference location Face to face challenge: Thursday 22 July 2010 Publication of the results during the Conference banquet. 
From: Daniel de Angelis Cordeiro <Daniel.Cordeiro@im...>  20100607 14:09:40

 CALL FOR PARTICIPATION PASCO 2010 International Workshop on Parallel Symbolic Computation 2010 Grenoble University, INRIA and CNRS Grenoble, France, July 2123, 2010 http://pasco2010.imag.fr/  The "2010 International Workshop on Parallel and Symbolic Computation" (PASCO) is the 4th meeting in a series of workshops dedicated to the promotion and advancement of parallel algorithms and software in all areas of symbolic mathematical computation. Following previous editions, PASCO 2010 will have presentations of accepted research papers and extended abstracts, invited talks, tutorial courses. Moreover, a programming contest will take place during the conference. * PASCO 2010 online registration is now available at http://pasco2010.imag.fr/ Early Registration (by June 30th) ACM/SIGSAM Members 190 EUR NonACM/SIGSAM Members 210 EUR Students 60 EUR Late and OnSite Registration ACM/SIGSAM Members 230 EUR NonACM/SIGSAM Members 250 EUR Students 90 EUR * Invited Lectures Christian Bertin (ST) & ClaudePierre Jeannerod, (INRIA), France. Techniques and tools for implementing IEEE 754 floatingpoint arithmetic on VLIW integer processors. Erich L. Kaltofen , North Carolina State University, USA. 15 years after DSC and WLSS2: what parallel computations I do today. Stephen T. LewinBerlin, Quanta Research Cambridge, USA. Exploiting Multicore Systems with Cilk * Tutorials Jeremy Johnson , Drexel University, USA. Automatic Performance Tuning. Daniel Kunkle , Northeastern University, USA. Roomy: A System for Space Limited Computations. * Organization General coChairs: Marc MorenoMaza, University of Western Ontario, Canada and JeanLouis Roch, Grenoble University, France. Local Arrangement Chairs: JeanGuillaume Dumas, Grenoble University, France and Thierry Gautier, INRIA, France and Clement Pernet, Grenoble University, France. Administration Chair: Daniele Herzog, INRIA France. Publicity Chair: Daniel Cordeiro, Grenoble University, France.  
From: Daniel de Angelis Cordeiro <Daniel.Cordeiro@im...>  20100329 14:10:42

(Please accept our apologies if you receive this message multiple times)  Parallel Symbolic Computation 2010 (PASCO 2010) July 2123, 2010  Grenoble, France http://pasco2010.imag.fr/ Third Announcement and C A L L f o r P A P E R S *** Submission date extended to April 18 *** Overview: The International Workshop on Parallel and Symbolic Computation (PASCO) is a series of workshops dedicated to the promotion and advancement of parallel algorithms and software in all areas of symbolic mathematical computation. The pervasive ubiquity of parallel architectures and memory hierarchy has led to the emergence of a new quest for parallel mathematical algorithms and software capable of exploiting the various levels of parallelism: from hardware acceleration technologies (multi core and multiprocessor system on chip, GPGPU, FPGA) to cluster and global computing platforms. To push up the limits of symbolic and algebraic computations, beyond the optimization of the application itself, the effective use of a large number of resources memory and general or specialized computing units is expected to enhance the performance multicriteria objectives: time, energy consumption, resource usage, reliability. In this context, the design and the implementation of mathematical algorithms with provable and adaptive performances is a major challenge. Earlier meetings in the PASCO series include PASCO'94 (Linz, Austria), PASCO'97 (Maui, U.S.A.), PASCO'07 (London, Canada). PASCO 2010 is affiliated with the 2010 International Symposium on Symbolic and Algebraic Computation (ISSAC) in Munich, Germany. Immediately prior to the ISSAC 2010 meeting, PASCO will be held in Grenoble, France. The workshop PASCO 2010 will be a threeday event including invited presentations and tutorials, contributed research papers and posters, and a programming contest. Specific topics include, but are not limited to: * Design and analysis of parallel algorithms for computer algebra * Practical parallel implementation of symbolic or symbolicnumeric algorithms * Highperformance software tools and libraries for computer algebra * Applications of highperformance computer algebra * Distributed datastructures for computer algebra * Hardware acceleration technologies (multicores, GPUs, FPGAs) applied to computer algebra * Cache complexity and cacheoblivious algorithms for computer algebra * Compiletime and runtime techniques for automating optimization and platform adaptation of computer algebra algorithms Call for Papers: The conference invites submission of papers presenting original research, either in the form of extended abstracts (2 pages) or full papers (up to 10 pages) in ACM format. As in previous years, PASCO 2010 will publish formal proceedings of the accepted papers. The PASCO 2010 Conference proceedings will be published by the Association for Computing Machinery (ACM) http://www.acm.org/ and will be made available in the ACM Digital Library. The proceedings will also be distributed on CDs to the participants of the workshop. Programming Contest: A programming contest will be organized during the PASCO 2010 meeting. Each participating team will be competing on one or more programming challenges proposed by the organizing committee and by the participants. Details can be found at the PASCO 2010 web site. Important Dates: (extended w.r.t. previous calls for papers) Paper submission deadline: April 18 (Sun), 2010 Programming Challenge proposal April 18 (Sun), 2010 Notification of acceptance: May 31 (Mon), 2010 (for papers and challenge proposals) Cameraready version of paper due: June 13 (Sun), 2010 Intent of participation to the contest: June 13 (Sun), 2010 Tutorials and Workshop in Grenoble: July 2123 (WedFri), 2010 Conference Chairs: Marc Moreno Maza (University of Western Ontario, Canada) <moreno@...> JeanLouis Roch (Grenoble University, France) <jlroch@...> Local Arrangements Chairs: JeanGuillaume Dumas (Grenoble University, France) <jeanguillaume.dumas@...> Thierry Gautier (INRIA Grenoble, France) <thierry.gautier@...> Clement Pernet (Grenoble University, France) <clement.pernet@...> Publicity Chair: Daniel Cordeiro (Grenoble University, France) <daniel.cordeiro@...> Administration: Daniele Herzog (INRIA Grenoble, France) <daniele.herzog@...> Christian Seguy (CNRS, France) <christian.seguy@...> Ahlem ZammitBoubaker (INRIA Grenoble, France) <ahlem.zammitboubaker@...> Program Committee: Daniel Augot (INRIA Saclay, France) JeanClaude Bajard (Montpellier II University, France) Olivier Beaumont (INRIA Bordeaux, France) Bruce Char (Drexel University, USA) Gene Cooperman (Northeastern University, USA) Gabriel DosReis (Texas A&M University, USA) JeanChristophe Dubacq (LIPN, University Paris 13, France) JeanGuillaume Dumas (Grenoble University, France) JeanCharles Faugere (INRIA  UPMC, France) Matteo Frigo (Axis Semiconductor, USA) Thierry Gautier (INRIA Grenoble, France) Pascal Giorgi (LIRMM, France) Stef Graillat (University Paris 6, France) Jeremy Johnson (Drexel University, USA) Erich Kaltofen (NCSU, USA) Herbert Kuchen (University of Muenster, Germany) Philippe Langlois (University of Perpignan, France) Anton Leykin (Georgia Tech, USA) Gennadi Malaschonok (Tambov State University, Russia) Michael Monagan (Simon Fraiser University, Canada) Winfried Neun (Zuse Institute Berlin, Germany) Clement Pernet (Grenoble University, France) Nicolas Pinto (MIT, USA) Manuel PrietoMatias (Complutense university of Madrid, Spain) Markus Pueschel (Carnegie Mellon University, USA) Nathalie Revol (INRIA  LIP, France) David Saunders (University of Delaware, USA) Eric Schost (University of Western Ontario, Canada) Wolfgang Schreiner (RISC, Austria) Arne Storjohann (University of Waterloo, Canada) Sivan Toledo (TelAviv University, Israel) Gilles Villard (CNRS, France) Yuzhen Xie (University of Western Ontario, Canada) Kazuhiro Yokoyama (Rikkyo University, Japan) Links: PASCO 2010 http://pasco2010.imag.fr/ ISSAC 2010 http://www.issacconference.org/2010/ Submission http://www.easychair.org/conferences/?conf=pasco2010 
From: Gabriel Dos Reis <gdr@cs...>  20100311 15:08:14

[Apologies for possible multiple postings.]  CALL FOR PAPERS  In cooperation with ACM SIGSAM, the International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS 2010) Part of CICM2010, in CNAM, Paris, France; 8th of July 2010  Important Dates  * Abstract submission: Fri 26 March 2010 * Paper submission: Fri 9 April 2010 * Reviews sent to authors: Mon 10 May 2010 * Author's response deadline: Mon 17 May 2010 * Notification of acceptance: Mon 24 May 2010 * Camera ready copy due: Mon 7 June 2010 * Workshop: Thu 8 July 2010 Invited Speaker: Jacques Carette (McMaster University, Canada) PLMMS Scope  The program committee welcomes submissions on programming language issues related to all aspects of mechanised mathematics systems (MMS). In particular:  Mathematical algorithms  Tactics and proof search  Proofs  Mathematical notation Of particular interest are the dimensions of:  Expressiveness  Efficiency  Correctness  Understandability and Usability  Modularity and Extensibility  Design and implementation Mechanised mathematics systems, whether standalone or embedded in larger systems, include but are not limited to:  Dependent typed programming languages  Proof assistants  Computer algebra systems  Proof planning systems  Theorem proving systems  Theory formation systems These issues have a very colourful history. Why are all the languages of mainstream computer algebra systems untyped? (Not for lack of trying: Axiom and Magma both enjoy type systems, although they have not (yet) become mainstream.) Why are the (strongly typed) proof assistants so much harder to use than a typical computer algebra systems? What forms of polymorphism exist in mathematics? What forms of dependent types may be used in mathematical modelling? How can MMS regain the upper hand on issues of "genericity" and "modularity"? What are the biggest barriers when using more mainstream languages for computer algebra systems, proof assistants or theorems provers? Many programming language innovations appeared in either computer algebra or proof systems first, before migrating into more mainstream programming languages. This workshop is an opportunity to present the latest innovations in the design of MMS that may be relevant to future programming languages, or conversely novel programming language principles that improve upon the implementation and deployment of MMS. Submission Details  Accepted papers will appear in the ACM Digital Library. Papers should be submitted via the PLMMS 2010 easychair website: http://www.easychair.org/conferences/?conf=plmms2010 Submissions must describe original unpublished work which is not been submitted for publication elsewhere. At least one author of each accepted paper is expected to attend PLMMS 2010 and present her or his paper. Papers should be no more than 8 pages in length and are to be submitted in PDF format. They must conform to the ACM SIGPLAN style guidelines using 9point font size (see http://www.acm.org/sigs/sigplan/authorInformation.htm  this also provides latex templates). Each submission must also adhere to SIGPLAN's republication policy (http://www.sigplan.org/republicationpolicy.htm). Papers will be reviewed by at least three reviewers and the authors will have an opportunity for rebuttal by the response deadline. Links  * http://www.easychair.org/conferences/?conf=plmms2010 abstract and paper submission webpage * ttp://www.acm.org/sigs/sigplan/authorInformation.htm submission style guide * http://www.sigplan.org/republicationpolicy.htm republication policy * http://dream.inf.ed.ac.uk/events/plmms2010/ the PLMMS 2010 web site * http://cicm2010.cnam.fr/ the CICM 2010 conference web site Program Committee  * Thorsten Altenkirch (University of Nottingham, UK) * Serge Autexier (DFKI, Germany) * David Delahaye (CNAM, Paris, France) * James Davenport [PC cochair] (University of Bath, UK) * Lucas Dixon [PC cochair] (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) 
From: Daniel de Angelis Cordeiro <Daniel.Cordeiro@im...>  20100308 12:12:37

(Please accept our apologies if you receive this message multiple times)  Parallel Symbolic Computation 2010 (PASCO 2010) July 2123, 2010  Grenoble, France http://pasco2010.imag.fr/ Second Announcement and C A L L f o r P A P E R S News:  PASCO 2010 Programming contest  PASCO 2010 in cooperation with ACM Overview: The International Workshop on Parallel and Symbolic Computation (PASCO) is a series of workshops dedicated to the promotion and advancement of parallel algorithms and software in all areas of symbolic mathematical computation. The pervasive ubiquity of parallel architectures and memory hierarchy has led to the emergence of a new quest for parallel mathematical algorithms and software capable of exploiting the various levels of parallelism: from hardware acceleration technologies (multi core and multiprocessor system on chip, GPGPU, FPGA) to cluster and global computing platforms. To push up the limits of symbolic and algebraic computations, beyond the optimization of the application itself, the effective use of a large number of resources memory and general or specialized computing units is expected to enhance the performance multicriteria objectives: time, energy consumption, resource usage, reliability. In this context, the design and the implementation of mathematical algorithms with provable and adaptive performances is a major challenge. Earlier meetings in the PASCO series include PASCO'94 (Linz, Austria), PASCO'97 (Maui, U.S.A.), PASCO'07 (London, Canada). PASCO 2010 is affiliated with the 2010 International Symposium on Symbolic and Algebraic Computation (ISSAC) in Munich, Germany. Immediately prior to the ISSAC 2010 meeting, PASCO will be held in Grenoble, France. The workshop PASCO 2010 will be a threeday event including invited presentations and tutorials, contributed research papers and posters, and a programming contest. Specific topics include, but are not limited to: * Design and analysis of parallel algorithms for computer algebra * Practical parallel implementation of symbolic or symbolicnumeric algorithms * Highperformance software tools and libraries for computer algebra * Applications of highperformance computer algebra * Distributed datastructures for computer algebra * Hardware acceleration technologies (multicores, GPUs, FPGAs) applied to computer algebra * Cache complexity and cacheoblivious algorithms for computer algebra * Compiletime and runtime techniques for automating optimization and platform adaptation of computer algebra algorithms Call for Papers: The conference invites submission of papers presenting original research, either in the form of extended abstracts (2 pages) or full papers (up to 10 pages) in ACM format. As in previous years, PASCO 2010 will publish formal proceedings of the accepted papers. The PASCO 2010 Conference proceedings will be published by the Association for Computing Machinery (ACM) http://www.acm.org/ and will be made available in the ACM Digital Library. Programming Contest: A programming contest will be organized during the PASCO 2010 meeting. Each participating team will be competing on one or more programming challenges proposed by the organizing committee and by the participants. Details can be found at the PASCO 2010 web site. Important Dates Paper submission deadline: April 2 (Fri), 2010 Programming Challenge proposal April 2 (Fri), 2010 Notification of acceptance: May 10 (Mon), 2010 (for papers and challenge proposals) Cameraready version of paper due: May 28 (Fri), 2010 Intent of participation to the contest: May 28 (Fri), 2010 Tutorials and Workshop in Grenoble: July 2123 (WedFri), 2010 Conference Chairs: Marc Moreno Maza (University of Western Ontario, Canada) <moreno@...> JeanLouis Roch (Grenoble University, France) <jlroch@... Local Arrangements Chairs: JeanGuillaume Dumas (Grenoble University, France) <jeanguillaume.dumas@... Thierry Gautier (INRIA Grenoble, France) <thierry.gautier@...> Clement Pernet (Grenoble University, France) <clement.pernet@...> Publicity Chair: Daniel Cordeiro (Grenoble University, France) <daniel.cordeiro@...> Administration: Daniele Herzog (INRIA Grenoble, France) <daniele.herzog@...> Christian Seguy (CNRS, France) <christian.seguy@...> Ahlem ZammitBoubaker (INRIA Grenoble, France) <ahlem.zammitboubaker@...> Program Committee: Daniel Augot (INRIA Saclay, France) JeanClaude Bajard (Montpellier II University, France) Olivier Beaumont (INRIA Bordeaux, France) Bruce Char (Drexel University, USA) Gene Cooperman (Northeastern University, USA) Gabriel DosReis (Texas A&M University, USA) JeanChristophe Dubacq (LIPN, University Paris 13, France) JeanGuillaume Dumas (Grenoble University, France) JeanCharles Faugere (INRIA  UPMC, France) Matteo Frigo (Axis Semiconductor, USA) Thierry Gautier (INRIA Grenoble, France) Pascal Giorgi (LIRMM, France) Stef Graillat (University Paris 6, France) Jeremy Johnson (Drexel University, USA) Erich Kaltofen (NCSU, USA) Herbert Kuchen (University of Muenster, Germany) Philippe Langlois (University of Perpignan, France) Anton Leykin (Georgia Tech, USA) Gennadi Malaschonok (Tambov State University, Russia) Michael Monagan (Simon Fraiser University, Canada) Winfried Neun (Zuse Institute Berlin, Germany) Clement Pernet (Grenoble University, France) Nicolas Pinto (MIT, USA) Manuel PrietoMatias (Complutense university of Madrid, Spain) Markus Pueschel (Carnegie Mellon University, USA) Nathalie Revol (INRIA  LIP, France) David Saunders (University of Delaware, USA) Eric Schost (University of Western Ontario, Canada) Wolfgang Schreiner (RISC, Austria) Arne Storjohann (University of Waterloo, Canada) Sivan Toledo (TelAviv University, Israel) Gilles Villard (CNRS, France) Yuzhen Xie (University of Western Ontario, Canada) Kazuhiro Yokoyama (Rikkyo University, Japan) Links: PASCO 2010 http://pasco2010.imag.fr/ ISSAC 2010 http://www.issacconference.org/2010/ Submission http://www.easychair.org/conferences/?conf=pasco2010 
From: <david.delahaye@cn...>  20100118 21:09:11

[Apologies for crosspostings.]  CALCULEMUS 2010  First Call for Papers  17th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning CNAM, Paris, France, July 78, 2010 http://cicm2010.cnam.fr/calculemus/ 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. We seek original research papers for the upcoming Calculemus meeting, which 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 crossfertilisation 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 Papers on other topics closely related to the above research areas will also be welcomed for consideration. Submission ========== Theoretical and applied research papers on all topics within the scope of the symposium are invited. Submitted papers must be in English and must not exceed 15 pages for full papers and we suggest 10 pages for emerging trends extended abstracts (the upper limit is 20 pages, authors must provide at least a title and 200 word abstract). The title page should contain the title, author(s) with affiliation(s), email address(es), listing of keywords and abstract. The program committee will subject all full papers submitted to a peer review. Emerging trends papers will be lightly reviewed. Results must be unpublished. Papers should be prepared in LaTeX and formatted according to the requirements of the Springer's LNAI series (the corresponding style files can be downloaded from http://www.springer.de/comp/lncs/authors.html and are the same for LNCS and LNAI). The web page for electronic submission is: http://www.easychair.org/conferences/?conf=calculemus2010 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 SpringerVerlag. Extended abstracts on emerging trends will be published as a technical report of CEDRIC (CNAM/ENSIIE) and will be electronically available. Important Dates =============== For (reviewed) full paper submissions: Abstract submission: February 24, 2010 Submission deadline: March 3, 2010 Notification of acceptance: April 14, 2010 Camera ready copies due: April 28, 2010 For extended abstracts on emerging trends: Abstract submission: April 30, 2010 Submission deadline: May 7, 2010 Notification of acceptance: May 30, 2010 Camera ready copies due: June 7, 2010 The Calculemus conference is on July 78, 2009. 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) _______________________________________________ projectcalculemus mailing list projectcalculemus@... http://lists.jacobsuniversity.de/mailman/listinfo/projectcalculemus 
From: <verify2010@ma...>  20100116 21:07:39

[Apologies for possible multiple postings] CALL FOR PAPERS 6th International Verification Workshop (VERIFY2010) What are the verification problems? What are the deduction techniques? in connection with IJCAR2010 at FLoC2010 July 2021, 2010, Edinburgh, UK [http://www.mais.informatik.tudarmstadt.de/verify2010/] ********************* Keynote speakers ****************************** ** Véronique Cortier (LORIA INRIALorraine, France) ** ** Cliff Jones (Newcastle University, UK) ** ** André Platzer (Carnegie Mellon University, USA) ** ********************************************************************** The formal verification of critical information systems has a long tradition as one of the main areas of application for automated theorem proving. Nevertheless, the area is of still growing importance as the number of computers affecting everyday life and the complexity of these systems are both increasing. The purpose of the VERIFY workshop series is to discuss problems arising during the formal modeling and verification of information systems and to investigate suitable solutions. Possible perspectives include those of automated theorem proving, tool support, system engineering, and applications. The VERIFY workshops aim at bringing together people who are interested in the development of safety and security critical systems, in formal methods, in the development of automated theorem proving techniques, and in the development of tool support. Practical experiences gained in realistic verifications are of interest to the automated theorem proving community and new theorem proving techniques should be transferred into practice. The overall objective of the VERIFY workshops is to identify open problems and to discuss possible solutions under the theme What are the verification problems? What are the deduction techniques? The scope of VERIFY includes topics such as + ATP techniques in verification + Information flow security + Case studies + Integration of ATPs and CASEtools (specification and verification) + Management of change + Combination of verification systems + Refinement and decomposition + Compositional and modular reasoning + Reliability of mobile computing + Experience reports on using + Reuse of specifications and proofs formal methods + Safetycritical systems + Formal methods for fault tolerance + Security models + Gaps between problems and + Tool support for formal methods techniques Submissions are encouraged in one of the following two categories: A. Regular papers: Submissions in this category should describe previously unpublished work (completed or in progress), including descriptions of research, tools, and applications. Papers must be 615 pages long, formatted following the Springer LNCS guidelines. B. Discussion papers: Submissions in this category are intended to initiate discussions and should address controversial issues, and may include provocative statements. Papers must be 315 pages long, formatted following the Springer LNCS guidelines. Submission of papers is via EasyChair: http://www.easychair.org/conferences/?conf=verify2010 Upon submission, the category (either A or B) should be indicated. Each accepted paper shall be presented at the workshop and at least one author of each paper must attend the workshop. In addition to informal proceedings, we envisage a special issue in a journal on the topic of the workshop. Participants of VERIFY2010 are particularly encouraged to submit a paper to the special issue, but other submissions will also be welcome. Program & Workshop CoChairs M. Aderhold (TU Darmstadt) S. Autexier (DFKI Bremen) H. Mantel (TU Darmstadt) Program Committee B. Beckert (Karlsruhe Institute of Technology) I. Cervesato (Carnegie Mellon University) C. Fournet (Microsoft Research) J. Guttman (Worcester Polytechnic Institute) R. Hähnle (Chalmers University) J. Hurd (Galois Inc.) D. Hutter (DFKI Bremen) P. Jackson (University of Edinburgh) C. Jones (Newcastle University) D. Kapur (University of New Mexico) J.P. Katoen (RWTH Aachen) G. Klein (NICTA) G. Lowe (University of Oxford) F. Martinelli (CNR Pisa) C. Meadows (Naval Research Laboratory) D. Pichardie (INRIA Rennes) G. Schneider (University of Gothenburg) J. Schumann (NASA Ames Research Center) C. Walther (TU Darmstadt) Important dates: Submission deadline: March 22, 2010 Notification of acceptance: April 29, 2010 Final version due: May 17, 2010 Workshop date: July 2021, 2010 Workshop email: verify2010@... 
From: Gabriel Dos Reis <gdr@cs...>  20100107 15:42:12

Reminder:  The submission deadline for ISSAC 2010 is soon approaching. If you intend to submit a paper, please submit a brief abstract at http://www.easychair.org/conferences/?conf=issac2010 by January 14. The full paper can be submitted at the same time or, up to a week later, by January 21. The Call for Papers is available at http://www.issacconference.org/2010/callforpapers/ News:  If you have not recently visited the conference web site, you may be interested that the invited speakers and tutorials have been announced. The invited speakers are: * Evelyne Hubert (INRIA Sophia Antipolis, France): Algebraic invariants and their differential algebras * Siegfried M. Rump (Hamburg U. of Technology, Germany & Waseda U., Japan): Verification methods: Rigorous results using floatingpoint arithmetic * Ashish Tiwari (SRI International, USA): Theory of reals for verification and synthesis of hybrid dynamical systems and the tutorials are: * Moulay A. Barkatou (Limoges U., France): Symbolic methods for solving systems of linear ordinary differential equations * Jürgen Gerhard (Maplesoft, Canada): Asymptotically fast algorithms for modern computer algebra * Sergey P. Tsarev (Siberian Federal U., Russia): Transformation and factorization of partial differential systems with applications to stochastic systems For details, please visit http://www.issacconference.org/2010 . Best regards, Peter Horn, on behalf of the ISSAC 2010 organizing committee PS: Apologies for multiple copies. 
From: Peter Horn <publicity2010@is...>  20100107 15:29:31

Reminder:  The submission deadline for ISSAC 2010 is soon approaching. If you intend to submit a paper, please submit a brief abstract at http://www.easychair.org/conferences/?conf=issac2010 by January 14. The full paper can be submitted at the same time or, up to a week later, by January 21. The Call for Papers is available at http://www.issacconference.org/2010/callforpapers/ News:  If you have not recently visited the conference web site, you may be interested that the invited speakers and tutorials have been announced. The invited speakers are: * Evelyne Hubert (INRIA Sophia Antipolis, France): Algebraic invariants and their differential algebras * Siegfried M. Rump (Hamburg U. of Technology, Germany & Waseda U., Japan): Verification methods: Rigorous results using floatingpoint arithmetic * Ashish Tiwari (SRI International, USA): Theory of reals for verification and synthesis of hybrid dynamical systems and the tutorials are: * Moulay A. Barkatou (Limoges U., France): Symbolic methods for solving systems of linear ordinary differential equations * Jürgen Gerhard (Maplesoft, Canada): Asymptotically fast algorithms for modern computer algebra * Sergey P. Tsarev (Siberian Federal U., Russia): Transformation and factorization of partial differential systems with applications to stochastic systems For details, please visit http://www.issacconference.org/2010 . Best regards, Peter Horn, on behalf of the ISSAC 2010 organizing committee PS: Apologies for multiple copies. 
From: Gabriel Dos Reis <gdr@cs...>  20090804 12:50:26

Apologies for duplicates.  The ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems Munich, Germany; August 21, 2009 The ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems will be colocated with TPHOLs 2009. Registration for the PLMMS 2009 workshop is now open. Important Dates and Deadlines * Abstract submission: Now closed * Submission deadline: Now closed * Author notification: June 22, 2009 * Camera ready papers: July 15, 2009 * Registration: Open, http://tphols.in.tum.de/fee.html * Workshop: August 21, 2009 General Information The scope of this workshop is at the intersection of programming languages and mechanized mathematics systems. The latter category subsumes presentday computer algebra systems, interactive proof assistants, and automated theorem provers, all heading towards fully integrated mechanized mathematical assistants. Tentative Programme Friday, August 21 09:0010:00 Invited talk (Session Chair:) Georges Gonthier. Ssreflect: Structured Scripting for HigherOrder Theorem Proving 10:0010:40 Coffee break 10:4012:10 Session 1 (Session Chair:) Paulo F. Silva, Joost Visser, Jose Oliveira. Galois: A Language for Proofs Using Galois Connections and Fork Algebras Makarius Wenzel. Parallel Proof Checking in Isabelle/Isar Andrea Asperti, Wilmer Riccioti, Claudio Sacerdoti Coen, Enrico Tassi. A New Type for Tactics 12:1013:40 Lunch 13:4014:40 Invited tutorial (Session Chair:) Gabriel Dos Reis. OpenAxiom: A Categorial Platform for Scientific Computation 14:4015:10 Coffee Break 15:1016:10 Session 2 (Session Chair:) Joe Hurd. OpenTheory: Package Management for Higher Order Logic Theories Johannes Holzl. Proving Inequalities Over Reals With Computation in Isabelle/HOL 16:1017:00 Business meeting Evening Social Event Links * http://plmms09.cs.tamu.edu/, the PLMMS 2009 workshop web site * http://tphols.in.tum.de/, the THOPLs 2009 conference web site * http://tphols.in.tum.de/fee.html, registration site Programme Committee * Clemens Ballarin, aicas GmbH * Gabriel Dos Reis, Texas A&M University (CoChair) * JeanChristophe Filliâtre, CNRS Université Paris Sud * Predrag Janicic, University of Belgrade * Jaakko Järvi, Texas A&M University * Florina Piroi, Johannes Kepler University * Laurent Théry, INRIA Sophia Antipolis (CoChair) * Makarius Wenzel, Technische Universität München 
From: Gabriel Dos Reis <gdr@cs...>  20090428 09:48:17

The ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems PLMMS 2009 Munich, Germany; August 21, 2009 http://plmms09.cse.tamu.edu/ CALL FOR PAPERS The ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems will be colocated with TPHOLs 2009. Important Dates * Abstract submission : May 11, 2009 (Apia, Samoa time) * Submission deadline: May 18, 2009 (Apia, Samoa time) * Author notification: June 22, 2009 * Camera ready papers: July 10, 2009 * Workshop: August 21, 2009 General Information The scope of this workshop is at the intersection of programming languages (PL) and mechanized mathematics systems (MMS). The latter category subsumes presentday computer algebra systems (CAS), interactive proof assistants (PA), and automated theorem provers (ATP), all heading towards fully integrated mechanized mathematical assistants. Areas of interest include all aspects of PL and MMS that meet in the following topics, but not limited to: * Dedicated input languages for MMS: covers all aspects of languages intended for the user to deploy or extend the system, both algorithmic and declarative ones. Typical examples are tactic definition languages such as Ltac in Coq, mathematical proof languages as in Mizar or Isar, or specialized programming languages built into CA systems. * Mathematical modeling languages used for programming: covers the relation of logical descriptions vs. algorithmic content. For instance the logic of ACL2 extends a version of Lisp, that of Coq is close to Haskell, and some portions of HOL are similar to ML and Haskell, while Maple tries to do both simultaneously. Such mathematical languages offer rich specification capabilities, which are rarely available in regular programming languages. How can programming benefit from mathematical concepts, without limiting mathematics to the computational world view? * Programming languages with mathematical specifications: covers advanced mathematical concepts in programming languages that improve the expressive power of functional specifications, type systems, module systems etc. Programming languages with dependent types are of particular interest here, as is intentionality vs extensionality. * Language elements for program verification: covers specific means built into a language to facilitate correctness proofs using MMS. For example, logical annotations within programs may be turned into verification conditions to be solved in a proof assistant eventually. How need MMS and PL to be improved to make this work conveniently and in a mathematically appealing way? These issues have a very colorful history. Many PL innovations first appeared in either CA or proof systems first, before migrating into more mainstream programming languages. This workshop is an opportunity to present the latest innovations in MMS design that may be relevant to future programming languages, or conversely novel PL principles that improve upon implementation and deployment of MMS. Why are all the languages of mainstream CA systems untyped? Why are the (strongly typed) proof assistants so much harder to use than a typical CAS? What forms of polymorphism exist in mathematics? What forms of dependent types may be used in mathematical modeling? How can MMS regain the upper hand on issues of "genericity" and "modularity"? What are the biggest barriers to using a more mainstream language as a host language for a CAS or PA/ATP? PLMMS 2007 was held as a satellite event of, and PLMMS 2008 was a CICM 2008 workshop. Submission Details Submitted papers should be in portable document format (PDF), formatted using the ACM SIGPLAN style guidelines (http://www.acm.org/sigs/sigplan/authorInformation.htm). The length is restricted to 10 pages, and the font size 9pt. Each submission must adhere to SIGPLAN's republication policy, as explained on the web. Violation risks summary rejection of the offending submission. Papers are exclusively submitted via EasyChair http://www.easychair.org/conferences?conf=plmms09 We expect that at least one author of each accepted paper attends PLMMS 2009 and presents her or his paper. Accepted papers will appear in the ACM Digital Library. Links * http://plmms09.cse.tamu.edu/, the PLMMS 2009 workshop web site * http://tphols.in.tum.de/, the THOPLs 2009 conference web site Program Committee * Clemens Ballarin, aicas GmbH * Gabriel Dos Reis, Texas A&M University (CoChair) * JeanChristophe Filliâtre, CNRS Université Paris Sud * Predrag Janicic, University of Belgrade * Jaakko Järvi, Texas A&M University * Florina Piroi, Johannes Kepler University * Laurent Théry, INRIA Sophia Antipolis (CoChair) * Makarius Wenzel, Technische Universität München 
From: Gabriel Dos Reis <gdr@cs...>  20090423 17:48:54

FYI. From: John R Harrison <johnh@...> Subject: My automated theorem proving textbook is now available Date: Tue, 21 Apr 2009 20:35:50 0700 For some time I've been working on a textbook giving a survey of some of the main results in automated theorem proving together with an introduction to basic mathematical logic. All the automated theorem proving techniques described are accompanied by actual OCaml code that the reader can use, modify and otherwise experiment with. I'm pleased to announce that the book has now been published. Handbook of Practical Logic and Automated Reasoning John Harrison Cambridge University Press 2009 ISBN: 9780521899574 Publisher's Web page: http://www.cambridge.org/9780521899574 Code and resources: http://www.cl.cam.ac.uk/~jrh13/atp/ Copies are already becoming available: you can order it directly from the publisher or from various other sources. Currently the price and availability looks a bit better in Europe (it was on offer for 56 pounds last week on amazon.co.uk). Here's a table of contents: 1 Introduction 1.1 What is logical reasoning? 1.2 Calculemus! 1.3 Symbolism 1.4 Boole's algebra of logic 1.5 Syntax and semantics 1.6 Symbolic computation and OCaml 1.7 Parsing 1.8 Prettyprinting 2 Propositional Logic 2.1 The syntax of propositional logic 2.2 The semantics of propositional logic 2.3 Validity, satisfiability and tautology 2.4 The De Morgan laws, adequacy and duality 2.5 Simplification and negation normal form 2.6 Disjunctive and conjunctive normal forms 2.7 Applications of propositional logic 2.8 Definitional CNF 2.9 The DavisPutnam procedure 2.10 Staalmarck's method 2.11 Binary Decision Diagrams 2.12 Compactness 3 Firstorder logic 3.1 Firstorder logic and its implementation 3.2 Parsing and printing 3.3 The semantics of firstorder logic 3.4 Syntax operations 3.5 Prenex normal form 3.6 Skolemization 3.7 Canonical models 3.8 Mechanizing Herbrand's theorem 3.9 Unification 3.10 Tableaux 3.11 Resolution 3.12 Subsumption and replacement 3.13 Refinements of resolution 3.14 Horn clauses and Prolog 3.15 Model elimination 3.16 More firstorder metatheorems 4 Equality 4.1 Equality axioms 4.2 Categoricity and elementary equivalence 4.3 Equational logic and completeness theorems 4.4 Congruence closure 4.5 Rewriting 4.6 Termination orderings 4.7 KnuthBendix completion 4.8 Equality elimination 4.9 Paramodulation 5 Decidable problems 5.1 The decision problem 5.2 The AE fragment 5.3 Miniscoping and the monadic fragment 5.4 Syllogisms 5.5 The finite model property 5.6 Quantifier elimination 5.7 Presburger arithmetic 5.8 The complex numbers 5.9 The real numbers 5.10 Rings, ideals and word problems 5.11 Groebner bases 5.12 Geometric theorem proving 5.13 Combining decision procedures 6 Interactive theorem proving 6.1 Humanoriented methods 6.2 Interactive provers and proof checkers 6.3 Proof systems for firstorder logic 6.4 LCF implementation of firstorder logic 6.5 Propositional derived rules 6.6 Proving tautologies by inference 6.7 Firstorder derived rules 6.8 Firstorder proof by inference 6.9 Interactive proof styles 7 Limitations 7.1 Hilbert's programme 7.2 Tarski's theorem on the undefinability of truth 7.3 Incompleteness of axiom systems 7.4 Goedel's incompleteness theorem 7.5 Definability and decidability 7.6 Church's theorem 7.7 Further limitative results 7.8 Retrospective: the nature of logic John Harrison. 
From: Gabriel Dos Reis <gdr@cs...>  20090403 11:40:58

The ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems PLMMS 2009 Munich, Germany; August 21, 2009 http://plmms09.cse.tamu.edu/ CALL FOR PAPERS The ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems will be colocated with TPHOLs 2009. General Information The scope of this workshop is at the intersection of programming languages (PL) and mechanized mathematics systems (MMS). The latter category subsumes presentday computer algebra systems (CAS), interactive proof assistants (PA), and automated theorem provers (ATP), all heading towards fully integrated mechanized mathematical assistants. Areas of interest include all aspects of PL and MMS that meet in the following topics, but not limited to: * Dedicated input languages for MMS: covers all aspects of languages intended for the user to deploy or extend the system, both algorithmic and declarative ones. Typical examples are tactic definition languages such as Ltac in Coq, mathematical proof languages as in Mizar or Isar, or specialized programming languages built into CA systems. * Mathematical modeling languages used for programming: covers the relation of logical descriptions vs. algorithmic content. For instance the logic of ACL2 extends a version of Lisp, that of Coq is close to Haskell, and some portions of HOL are similar to ML and Haskell, while Maple tries to do both simultaneously. Such mathematical languages offer rich specification capabilities, which are rarely available in regular programming languages. How can programming benefit from mathematical concepts, without limiting mathematics to the computational world view? * Programming languages with mathematical specifications: covers advanced mathematical concepts in programming languages that improve the expressive power of functional specifications, type systems, module systems etc. Programming languages with dependent types are of particular interest here, as is intentionality vs extensionality. * Language elements for program verification: covers specific means built into a language to facilitate correctness proofs using MMS. For example, logical annotations within programs may be turned into verification conditions to be solved in a proof assistant eventually. How need MMS and PL to be improved to make this work conveniently and in a mathematically appealing way? These issues have a very colorful history. Many PL innovations first appeared in either CA or proof systems first, before migrating into more mainstream programming languages. This workshop is an opportunity to present the latest innovations in MMS design that may be relevant to future programming languages, or conversely novel PL principles that improve upon implementation and deployment of MMS. Why are all the languages of mainstream CA systems untyped? Why are the (strongly typed) proof assistants so much harder to use than a typical CAS? What forms of polymorphism exist in mathematics? What forms of dependent types may be used in mathematical modeling? How can MMS regain the upper hand on issues of "genericity" and "modularity"? What are the biggest barriers to using a more mainstream language as a host language for a CAS or PA/ATP? PLMMS 2007 was held as a satellite event of, and PLMMS 2008 was a CICM 2008 workshop. Submission Details * Submission deadline: May 11, 2009 (Apia, Samoa time) * Author Notification: June 22, 2009 * Final Papers Due: July 10, 2009 * Workshop: August 21, 2009 Submitted papers should be in portable document format (PDF), formatted using the ACM SIGPLAN style guidelines (http://www.acm.org/sigs/sigplan/authorInformation.htm). The length is restricted to 10 pages, and the font size 9pt. Each submission must adhere to SIGPLAN's republication policy, as explained on the web. Violation risks summary rejection of the offending submission. Papers are exclusively submitted via EasyChair http://www.easychair.org/conferences?conf=plmms09 We expect that at least one author of each accepted paper attends PLMMS 2009 and presents her or his paper. Accepted papers will appear in the ACM Digital Library. Links * http://plmms09.cse.tamu.edu/, the PLMMS 2009 workshop web site * http://tphols.in.tum.de/, the THOPLs 2009 conference web site Program Committee * Clemens Ballarin, aicas GmbH * Gabriel Dos Reis, Texas A&M University (CoChair) * JeanChristophe Filliâtre, CNRS Université Paris Sud * Predrag Janinic, University of Belgrade * Jaakko Järvi, Texas A&M University * Florina Piroi, Johannes Kepler University * Laurent Théry, INRIA Sophia Antipolis (CoChair) * Makarius Wenzel, Technische Universität München 
From: Gabriel Dos Reis <gdr@cs...>  20090325 20:02:00

The following message is a courtesy copy of an article that has been posted to sci.math.symbolic as well. I'm pleased to announce that OpenAxiom1.2.1 was released on January 29, 2009. OpenAxiom is an open source platform for scientific and engineering computation, with an emphasis on symbolic, numeric, and algebraic computation. This is a bug fix release with respect to previous OpenAxiom releases. This release adds improvements to the interpreter, the compiler, and the algebra set. More information on new features can be found at http://www.openaxiom.org/1.2/ OpenAxiom1.2.1 is known to build and run on major Unix systems, GNU/Linux systems, Windows (MinGW/MSYS), and handheld devices. The source code of OpenAxiom, and precompiled (Windows and Linux) binaries are available for download from http://www.openaxiom.org/download.html OpenAxiom is a free software released under a BSDtype license. For more information about OpenAxiom, please visit us at http://www.openaxiom.org/ Feel free to use our Bug Tracker https://sourceforge.net/tracker/?group_id=203172 to report issues related to uses, build, or installation of OpenAxiom, or requests for improvements. Drop us a note at openaxiomhelp@... I'm grateful to the people who helped improve this release and make it possible. In particular, Alfredo Portes helped with testing on Windows platform and provided Windows binaries. Aleksej Saushev has been instrumental with testing and fixing the build infrastructure on FreeBSD, NetBSD, and OpenBSD. Enjoy.  Gaby  Dr. Gabriel Dos Reis (gdr@...), Assistant Professor http://www.cs.tamu.edu/people/faculty/gdr Department of Computer Science & Engineering; TAMU 301, Bright Building  College Station, TX 778433112 
From: Gabriel Dos Reis <gdr@cs...>  20090226 16:04:50

I am pleased to announce the OpenMath Workshop 2009, to be held on 10 July 2009, at Grand Bend Ontario, in conjunction with CICM 09 (http://www.orcca.on.ca/conferences/cicm09/cicm09/). The call for papers is at http://staff.bath/ac.uk/masjhd/OM2009.xhtml Submission is via EasyChair (29 April for abstracts, 4 May for papers): http://www.easychair.org/conferences?conf=om2009 We look forward to seeing your contributions, and your content dictionaries! James Davenport OpenMath Content Dictionary Editor _______________________________________________ projectsmkmig mailing list projectsmkmig@... http://lists.jacobsuniversity.de/mailman/listinfo/projectsmkmig 
From: Gabriel Dos Reis <gdr@cs...>  20090219 00:30:40

Call for Papers: MathUI'09  Mathematical User Interfaces Workshop 2009  at the MKM conference, July 6th, Grand Bend Ontario Canada http://www.activemath.org/workshops/MathUI/09/ SCOPE The 5th mathematical userinterfaces workshop is a forum to discuss, demo, present, brainstorm, and review all the mathspecific facets of userinterfaces. It happens in the form of a peerreviewed workshop with presentations and discussion, followed by an expolike demosession. Programs for computerized mathematics are evolving rapidly and are being used by a wider audience than ever before. Researchers are aiming to provide welldesigned and widelyapplicable user interfaces for this diverse audience. Among the questions lies the hypothesis that unified mathematical language is used with all systems. Can we achieve this? This workshop provides a forum for the discussion of computer representations of mathematics, and how gestures, writing, speech, or other novel techniques can be used to improve mathematical user interfaces. Topics include:  presentations on manipulation of mathematical knowledge  workflow studies based on mathematical applications  user studies on the effectiveness of interfaces  interactive teaching and testing  novel, original or downright funky interfaces to mathematics software  interactive mathematics generally SUBMISSIONS We are seeking submissions of either papers on and/or demonstrations of user interfaces for mathematics. Videos, prototypes, mock ups and any other sort of demonstration are welcome! Proceedings will be online. Submission format: article of 38 (printed) pages, in PDF format only, which may include other electronic presentations such as videos or animations complemented by an abstract of less than 150 words. Important Dates:  Either submit your abstract on until May 1st 2009 and a paper on May 15th. or submit an paper on May 8th 2009  Be prepared for a rebuttal phase from May 25th till 30th  Expect an answer on June 2nd 2009  Enjoy the workshop on July 6th 2009 All submissions are done on MathUI's easychair. http://www.easychair.org/conferences/?conf=mathui09 PROGRAMME COMMITTEE The workshop will be reviewed by the following persons:  David Aspinall, Edinburgh, Scotland  Paul Cairns, York, Great Britain  Olga Caprotti, Helsinki, Finland  Richard Fateman, Berkeley, USA  Anthony Jameson, Saarbruecken, Germany  Paul Libbrecht (organizer), Saarbruecken, Germany  Robert Miner, Minneapolis, USA  Elena Smirnova, London, Canada Further information, please contact Paul Libbrecht, paul@... _______________________________________________ projectsmkmig mailing list projectsmkmig@... http://lists.jacobsuniversity.de/mailman/listinfo/projectsmkmig 
From: Gabriel Dos Reis <gdr@cs...>  20090209 00:23:50

From: Gabriel Dos Reis <gdr@cs...>  20090109 16:42:55

From: Gabriel Dos Reis <gdr@cs...>  20090107 19:42:47
