Ontario Research Centre for Computer Algebra
Conferences on Intelligent Computer Mathematics

16th Symposium on the Integration of
Symbolic Computation and Mechanised Reasoning

Calculemus 2009

Grand Bend, Ontario (CANADA), 06-07 July 2009
 CALCULEMUS 2009 - Final Call for Papers
16th Symposium on the Integration of
Symbolic Computation and Mechanised Reasoning

6-7 July 2009, Joint with CICM'09, Ontario, Canada.


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

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 MKM 2009 (confederated in the Conferences on Intelligent
Computer Mathematics, CICM 2009) in Ontario, Canada.


We are pleased to have invited talks from: 

Prof. Jacques Calmet (http://iaks-www.ira.uka.de/iaks-calmet/en_index.html)

Rob Arthan (Director of Lemma 1, developer of ProofPower,


The scope of Calculemus covers all aspects of the interplay of mechanised
reasoning and computer algebra, including cross-fertilisation between those two
research areas, as well as the development of integrated systems that transcend
both computer algebra and theorem proving. Potential topics of interest include:

* Theorem proving in computer algebra (CAS)
* Computer algebra in theorem proving (PA and ATP)
* Case studies and applications that both involve computer algebra and
mechanised reasoning
* Representation of mathematics in computer algebra
* Adding computational capabilities to PA and ATP
* Formal methods requiring mixed computing and proving
* Combining methods of symbolic computation and formal deduction
* Mathematical computation in PA and ATP
* Theory, design and implementation of interdisciplinary systems for
computer mathematics
* Infrastructure for mathematical services
* Theory exploration techniques

Papers on other topics closely related to the above research
areas will also be welcomed for consideration.


For (reviewed) full-paper submissions, the deadlines are:

Abstract submission: 13 February 2009
Submission deadline: 20 February 2009
Notification of acceptance: 10 April 2009
Camera ready copies due: 24 April 2009

For extended abstracts on emerging trends, the deadlines are:

Submission deadline: 7 May 2009
Notification of acceptance: 30 May 2009
Camera ready copies due: 12 June 2009

The dates of the Calculemus conference are: 6,7 July 2009


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 should be between 200 words and 20 pages for
emeging trends extended abstracts - we suggest 10 pages. The title page should
contain the title, author(s) with affiliation(s), e-mail address(es), listing of
keywords and abstract. The program committee (PC) will subject all full-papers
submitted to a peer review. Emerging trends papers will be lightly reviewed.
Results must be unpublished.

The web page for electronic submission of full-papers is:

The web page for electronic submission of emerging trends papers is:

The proceedings of full-papers in the conference will be published as a volume
in the series Lecture Notes in Artificial Intelligence (LNAI) by
Springer-Verlag. Accepted papers will have to 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).

Emerging trends papers will be made available online, but will not be published.
These papers are expected to be describing work in progress.

Markus Aderhold (TU Darmstadt, Germany)
Serge Autexier (DFKI, Germany)
John Campbell (University College London, UK)
Jacques Carette (PC Chair) (McMaster University, Canada)
James H. Davenport (University of Bath, UK)
Louise Dennis (University of Liverpool, UK)
Lucas Dixon (PC Chair) (University of Edinburgh, UK)
William Farmer (McMaster University, Canada)
Jacques Fleuriot (University of Edinburgh, UK)
Herman Geuvers (Radboud University Nijmegen, Netherlands)
Michael Kohlhase (DFKI, Germany)
Steve Linton (University of St. Andrews, UK)
Tomas Recio (Universidad de Cantabria, Spain)
Tom Ridge (University of Cambridge, UK)
Julio Rubio (Universidad de La Rioja, Spain)
Volker Sorge (University of Birmingham, UK)