[Agda] Deadline Extension March 12th, 2013: Conf. Intelligent Computer Mathematics (CICM 2013), July 8-12, 2013, Bath, UK

[Serge Autexier]

     CICM 2013 - Conferences on Intelligent Computer Mathematics
         July 8-12, 2013 at University of Bath, Bath, UK

           http://www.cicm-conference.org/2013/cicm.php

                         Call for Papers

-------------------------------------------------------------------
* Invited Talks by Patrick Ion, Assia Mahboubi, and Ursula Martin * 
-------------------------------------------------------------------

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 Conferences on Intelligent Computer Mathematics offers a
venue for discussing these areas and their synergy.

The conference will take place at the University of Bath (www.bath.ac.uk),
with James Davenport as the local organiser. It consists of four tracks:

Calculemus
  Chair: Wolfgang Windsteiger
Digital Mathematical Libraries (DML)
  Chair: Petr Sojka
Mathematical Knowledge Management (MKM)
  Chair: David Aspinall
Systems and Projects
  Chair: Christoph Lange

As in previous years, there are plans to organise a workshop for
presentations by Doctoral students.
  
The overall programme will be organised by the General Program Chair
Jacques Carette.

----------------------------------------------------------------
                             Important dates
----------------------------------------------------------------

Submission deadline:          12 March 2013 (EXTENDED)
Reviews sent to authors:      5 April 2013
Rebuttals due:                8 April 2013
Notification of acceptance:  14 April 2013
Camera ready copies due:     26 April 2013
Conference:                 8-12 July 2013

----------------------------------------------------------------
                               Tracks
----------------------------------------------------------------

==========
Calculemus
==========

Calculemus 2013 invites the submission of original research contributions
to be considered for publication and presentation at the conference.
Calculemus is a series of conferences dedicated to the integration of
computer algebra systems (CAS) and systems for mechanised reasoning like
interactive proof assistants (PA) or 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
mathematical assistant systems that will be used routinely by
mathematicians, computer scientists and all others who need
computer-supported mathematics in their every day business.

All topics in the intersection of computer algebra systems and automated
reasoning systems are of interest for Calculemus. These include but are not
limited to:

* Automated theorem proving in computer algebra systems.
* Computer algebra in theorem proving systems.
* Adding reasoning capabilities to computer algebra systems.
* Adding computational capabilities to theorem proving systems.
* Theory, design and implementation of interdisciplinary systems for
computer mathematics.
* Case studies and applications that involve a mix of computation and
reasoning.
* Case studies in formalization of mathematical theories.
* Representation of mathematics in computer algebra systems.
* Theory exploration techniques.
* Combining methods of symbolic computation and formal deduction.
* Input languages, programming languages, types and constraint languages,
and modeling languages for mathematical assistant systems.
* Homotopy type theory.
* Infrastructure for mathematical services.

===
DML
===

Mathematicians dream of a digital archive containing all peer-reviewed
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. 

Track objective is to provide a forum for development of math-aware 
technologies, standards, algorithms and formats towards fulfillment
of the dream of global digital mathematical library (DML). Computer
scientists (D) and librarians of digital age (L) are especially 
welcome to join mathematicians (M) and discuss many aspects of DML 
preparation. 

Track topics are all topics of mathematical knowledge management 
and digital libraries applicable in the context of DML building -- 
processing of math knowledge expressed in scientific papers in 
natural languages, namely:

* Math-aware text mining (math mining) and MSC classification
* Math-aware representations of mathematical knowledge
* Math-aware computational linguistics and corpora
* Math-aware tools for [meta]data and fulltext processing
* Math-aware OCR and document analysis
* Math-aware information retrieval
* Math-aware indexing and search
* Authoring languages and tools
* MathML, OpenMath, TeX and other mathematical content standards
* Web interfaces for DML content
* Mathematics on the web, math crawling and indexing
* Math-aware document processing workflows 
* Archives of written mathematics
* DML management, business models
* DML rights handling, funding, sustainability 
* DML content acquisition, validation and curation 

===
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 non-exclusive 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 presenting available systems and new and
ongoing projects in all areas and topics related to the CICM conferences:

* Deduction and Computer Algebra (Calculemus)
* Digital Mathematical Libraries (DML)
* Mathematical Knowledge Management (MKM)
* Artificial Intelligence and Symbolic Computation (AISC)

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.

----------------------------------------------------------------
                       Submission Instructions
----------------------------------------------------------------

Submissions to the research tracks 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.

System descriptions and projects descriptions should be 2-4 pages and
should present
* newly developed systems,
* systems that have not previously been presented to the CICM community,
  or
* significant updates to existing systems.
Systems must be available for download.

Project presentations 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.

Presentations of new projects should mention relevant previous work and
include a roadmap that outlines concrete steps. All submissions should
contain links to demos, downloadable systems, or project websites.

Accepted conference submissions from all tracks is intended to 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.

Work-in-progress 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 work-in-progress papers
instead. Depending on the number of work-in-progress papers accepted,
they will be presented at the conference either as short talks or as
posters. The work-in-progress proceedings will be published as a
technical report, as well as online with CEUR-WS.org.

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=cicm2013

----------------------------------------------------------------
                       Programme Committee
----------------------------------------------------------------

Jacques Carette, McMaster University, Canada
Wolfgang Windsteiger, RISC Institute, JKU Linz, Austria
Petr Sojka, Masaryk University, Faculty of Informatics, Czech Republic
David Aspinall, University of Edinburgh, UK
Christoph Lange, University of Birmingham, UK
Till Mossakowski, DFKI Bremen, Germany
Jónathan Heras, University of Dundee, UK
Josef Urban, Radboud University, Netherlands
Deyan Ginev, Jacobs University Bremen, Germany
Rob Arthan, Queen Mary University of London, UK
Makarius Wenzel, Université Paris-Sud 11, France
Hendrik Tews, TU Dresden, Germany
Simon Colton, Department of Computing, Imperial College, London, UK
Paul Libbrecht, Martin Luther University Halle-Wittenberg, Germany
Cezary Kaliszyk, University of Innsbruck, Austria
Andrea Kohlhase, Jacobs University Bremen, Germany
Yannis Haralambous, Télécom Bretagne, France 
Florian Rabe, Jacobs University Bremen, Germany
Akiko Aizawa, NII, The University of Tokyo, Japan
Carsten Schuermann, IT University of Copenhagen, Denmark
Magnus O. Myreen, University of Cambridge, UK
Janka Chlebíková, School of Computing, University of Portsmouth, UK
Richard Zanibbi, Rochester Institute of Technology, US
Michael Kohlhase, Jacobs University Bremen, Germany
Adam Kilgarriff, Lexical Computing Ltd, UK
Leo Freitas, Newcastle University, UK
Frank Tompa, University of Waterloo, Canada
Gudmund Grov, Heriot-Watt University, Edinburgh, UK
Jeremy Avigad, Carnegie Mellon University, US
Stephen Watt, University of Western Ontario, Canada
Temur Kutsia, RISC Institute, JKU Linz, Austria
Manfred Kerber, University of Birmingham, UK
Hoon Hong, North Carolina State University, US
Christoph Lüth, DFKI Bremen, Germany
Thierry Bouche, Université Joseph Fourier (Grenoble), France
Andrea Asperti, University of Bologna, Italy
Jesse Alama, CENTRIA, FCT, Universidade Nova de Lisboa, Portugal
Jiří Rákosník, Institute of Mathematics, Academy of Sciences, Czech Republic
Thomas Hales, University of Pittsburgh, US
Predrag Janičić, University of Belgrade, Serbia
David Ruddy, Cornell University Library, US
Volker Sorge, University of Birmingham, UK 
Mark Adams, Proof Technologies Ltd, UK
John Charnley, Department of Computing, Imperial College London, UK