Call for Papers

Digital and computational solutions are becoming the prevalent means for the generation, communication, processing, storage and curation of mathematical information. Separate communities have developed to investigate and build computer based systems for computer algebra, automated deduction, and mathematical publishing as well as novel user interfaces. While all of these systems excel in their own right, their integration can lead to synergies offering significant added value. The Conference on Intelligent Computer Mathematics (CICM) offers a venue for discussing and developing solutions to the great challenges posed by the integration of these diverse areas.

CICM has been held annually as a joint meeting since 2008, co-locating related conferences and workshops to advance work in these subjects. Previous meetings have been held in Birmingham (UK 2008), Grand Bend (Canada 2009), Paris (France 2010), Bertinoro (Italy 2011), Bremen (Germany 2012), Bath (UK 2013), Coimbra (Portugal 2014), and Washington DC (USA 2015)

This is a call for papers for CICM 2016, which will be held in Bialystok, Poland July 25-29, 2016.

The principal tracks of the conference will be:

• Track: Calculemus (chair: Leonardo de Moura)
• Track: Digital Mathematical Libraries (DML) (chair: Frank Tompa)
• Track: Mathematical Knowledge Management (MKM) (chair: Bruce Miller)
• Track: Systems & Data (chair: Moa Johansson)
• Track: Doctoral Programme (chair: Martin Suda)

The overall programme is organized by the General Program Chair Michael Kohlhase. The workshop and publicity chair is Serge Autexier. The local arrangements will be coordinated by Adam Naumowicz.

We plan to have proceedings of the conference as in previous years with Springer Verlag as a volume in Lecture Notes in Artificial Intelligence (LNAI).

As in previous years, it is anticipated that there will be a number co-located workshops, including one to mentor doctoral students giving presentations.

Important Dates

Doctoral Program submissions are by e-mail to the DP chair: Martin Suda.
Work-in-Progress submissions are via Easychair with the keyword Track: Work in Progress (and possibly the intended topical track).

Track Calculemus: Symbolic Computation and Mechanised Reasoning

Calculemus is dedicated to the integration of computer algebra systems (CAS) and systems for mechanized reasoning such as interactive proof assistants (PA) and automated theorem provers (ATP). Currently, symbolic computation is divided into several (more or less) independent branches: traditional ones (e.g., computer algebra and mechanized reasoning) as well as emerging ones (on user interfaces, knowledge management, theory exploration, symbolic execution, abstract interpretation, etc.) We wish to bring these developments together in order to facilitate the theory, design, and implementation of integrated systems. These systems should be convenient to use routinely by mathematicians, computer scientists and all others who need computer-supported mathematics in their daily work.

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 and symbolic computation 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 that include non-trivial computations.
• 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.

Track DML: Digital Mathematical Libraries

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.

The track objective is to provide a forum for the development of math-aware technologies, standards, algorithms, and formats that can lead towards fulfilling the dream of a global Digital Mathematical Library (DML). The DML track also serves as an interdisciplinary venue to share experience and best practices among projects in digital libraries, natural language processing, optical character recognition, pattern recognition, information retrieval, and other areas that could change the paradigm for creating, storing, preserving, searching, and interacting with a mathematical corpus.

Track topics span all aspects of DML creation, maintenance, and use, including (but not limited to):

• DML creation and maintenance (content acquisition, validation and curation)
  • Acquisition from paper sources (OCR and document analysis)
  • Acquisition from digital sources (crawling and indexing)
  • Formula and diagram recognition
  • DML authoring languages and tools
  • Content extraction (math mining)
  • Classification, including application of MSC
  • DML management, including business models and funding
  • Digital rights management
  • Preservation and sustainability
• DML architecture and representations
  • Centralized and distributed libraries
  • Representations of mathematical content, including mathematical content standards
  • Metadata content and management
• DML access and applications
  • Mathematics retrieval
  • Web interfaces for DML content
  • User and application program interfaces (UIs and APIs)
  • Document processing workflows
• DML collections and systems
  • Archives of written mathematics
  • Experience from running existing DMLs

All accepted papers will address problems that arise specifically in the context of mathematical content. Nevertheless, authors of contributions that rely on sophisticated mathematical knowledge and algorithms might consider submitting their papers to the Mathematical Knowledge Management (MKM) track. Authors who wish to describe prototype DML systems and projects might consider submitting complementary papers to the Systems and Data track.

Track MKM: Mathematical Knowledge Management

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 track is concerned with all aspects of mathematical knowledge management. A non-exclusive list of important topics includes:

• Representations of mathematical knowledge
  • ranging from formal to informal
  • for mathematical formula or meta-knowledge about mathematics
  • standards including MathML, OpenMath, Content Dictionaries
  • presentation of mathematics on the web and elsewhere
• Creation and discovery of mathematical knowledge
  • Authoring languages and tools, OCR
  • Collaboration tools for mathematics
  • Data mining, theory exploration
• Methods for managing, storing, discovering and manipulating mathematical knowledge
  • Analysis and deduction systems (CAS, ATP)
  • Mathematical search and retrieval; repositories and access
  • Math assistants, tutoring and assessment systems
  • Challenges and solutions for mathematical work-flows

The interests of the MKM Track of CICM necessarily, and intentionally, overlap those of other CICM tracks but generally with a broader point of view. Authors of papers dealing more specifically with Theorem Proving or Mathematical Libraries may consider submitting to the Calculemus or DML tracks, respectively. Work involving prototypes of or enhancements to systems may wish to submit to the Systems and Data track, possibly as a complementary paper.

Track: Systems and Data

The systems and data track provides a forum to publish digital resources whose value cannot be adequately represented by a printed paper alone. It aims at an exchange of ideas between developers and users in any area related to the CICM conferences.

Systems can be for example stand-alone; plugins, libraries, or extensions of existing systems; or integrations of existing systems. Data can be for example formalizations; harvests or new processing of existing data; or case studies, test cases, or benchmark suites for systems.

In either case, the primary evaluation criteria are the

1. novelty,
2. value, and
3. usability,

of the system/data and the

4. clarity of the accompanying paper (up to 6 pages).

Detailed comments:

1. Resources are considered novel if they are not the primary focus of a previous archival publication or a concurrent submission. They may also be considered novel if they are substantially more mature than precursors that supported previous archival publications.
   It is possible to supplement a regular submission in another track with a system/data submission if both are valuable independently and can be reviewed and published separately. Authors must point this out in both submissions.
2. The judgement of the value of a submission is at the discretion of the PC.
3. Reviewers must be able to try out and use all systems/data conveniently. In particular,
   • the system/data must be available online with clear instructions for download, installation, etc. on the website,
   • the prerequisites (e.g., the system to process the data) must be clearly described on the website,
   • unusual prerequisites and non-default configurations should be bundled,
   • resources should be open source.
4. Authors must accompany their submission with a printable paper that will appear in the proceedings. This paper should outline the motivation, design decisions, and applications of the system/data. It must include the online reference to the system/data, and examples, screenshots, etc. given in the paper must be consistent with the digital resource.

Projects and Surveys

CICM strongly encourages the submission of project and survey papers.

Project papers (max. 4-15 pages, according to the scope and impact of the project) have a broader scope than regular papers (and consequently tend to present results at less depth). Papers on past projects may contain previously published results if their coherent presentation in a single paper provides new value. Papers on current projects may contain envisioned results if these are valuable to shape future research. Project papers can range from:

• projects that are new or about to start,
• ongoing projects that have not yet been presented to the CICM community, to
• 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 project submissions must have a live project website and should contain links to demos, videos, downloadable systems or downloadable datasets. Submission of descriptions of new projects are encouraged but would typically be classified as work in progress. We especially solicit for papers of long standing projects. Projects will be evaluated within the main tracks and will be published in the main proceedings.

Survey papers (max. 15 pages) present a relevant research problem and discuss, compare, or evaluate historical and/or state-of-the-art solutions. Surveys should be as comprehensive and objective as possible. The discussed research may or may not include research by the authors of the survey.

For project and survey papers, the PC will judge the merits of the paper on a case-by-case basis.

Submission Instructions

Electronic submission is done through EasyChair. 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.

Submissions to the research tracks (Calculemus, DML, MKM) must not exceed 15 pages in the LNCS style 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 and Data descriptions must not exceed 4 pages in the LNCS style.

A project description should be between 4 and 15 pages, depending on the size and impact of the project.

Details of the publication are to be determined. We currently plan that the 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.

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 paper for a research track or system description. This includes work in progress and emerging trends. Their size is not limited, but we recommend 5-10 pages.

Work-in-Progress submissions are via Easychair with the keyword Track: Work in Progress (and possibly the intended topical track).

The programme committee may offer authors of rejected formal submissions the opportunity 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.

Doctoral Programme

CICM is an excellent opportunity for graduate students to meet established researchers from the areas of computer algebra, automated deduction, and mathematical publishing.

The Doctoral Programme provides a dedicated forum for PhD students to present and discuss their ideas, ongoing or planned research, and achieved results in an open atmosphere. It will consist of presentations by the PhD students to get constructive feedback, advice, and suggestions from the research advisory board, researchers, and other PhD students. Each PhD student will be assigned to an experienced researcher from the research advisory board who will act as a mentor and who will provide detailed feedback and advice on their intended and ongoing research.

Students at any stage of their PhD can apply and should submit the following documents by e-mail to the DP chair: Martin Suda.:

A two-page abstract of the thesis describing the research questions, research plans, completed and remaining research, evaluation plans and publication plans; A two-page CV that includes background information (name, university, supervisor), education (degree sought, year/status of degree, previous degrees), employments, relevant research experience (publications, presentations, attended conferences or workshops, etc.)

Submission Deadline: 1. May 2016

Programme Committee

General chair

• Michael Kohlhase (Jaocbs University Bremen)

Calculemus track

• Leonardo de Moura (Microsoft; Chair)
• Georges Gonthier (Microsoft Research, UK)
• Ursula Martin (Oxford University, UK)
• Jacques Carette (McMaster University, CA)
• Lawrence Paulson (Cambridge University, UK)
• Assia Mahboubi (INRIA, France)
• Christopher Brown (US Naval Academy)
• Adam Strzebonski (Wolfram Inc.)
• James Davenport (University of Bath, UK)

DML track

• Frank Tompa (University of Waterloo; Chair)
• Akiko Aizawa (NII and University of Tokyo, Japan)
• Thiery Bouche (University Grenoble, France)
• Yannis Haralambous, Inst Mines-Télécom (Télécom Bretagne, France)
• Joe Corneli (Goldsmiths College, UK)
• Jim Pitman (UC Berkeley, USA)
• Petr Sojka (Masaryk University, CZ)
• Volker Sorge (University of Birmingham, UK)
• Abdou Youssef (George Washington University, USA)

MKM track

• Bruce Miller (NIST; Chair)
• Cezary Kaliszyk (Innsbruck University, Austria)
• Christoph Lange (Fraunhofer Bonn, Germany)
• David Aspinall (The University of Edinburgh, UK)
• Florian Rabe (Jacobs University, Germany)
• Gudmund Grov (Heriot Watt University, UK)
• Elena Smirnova (Texas Instruments, USA)
• Andrea Asperti (University of Bologna, Italy)
• Richard Zanibbi (Rochester Institute of Technology, USA)

Systems and Data track

• Moa Johansson (Chalmers University, Sweden; Chair)
• Serge Autexier (DFKI Bermen, Germany)
• Mateja Jamnik (Cambridge University, UK)
• Andrea Kohlhase (University of Applied Sciences, Neu Ulm, Germany)
• Laura Kovacs (Chalmers University, Sweden)
• Fiona McNeill (Heriot Watt University, UK)
• Nick Smallbone (Chalmers University, Sweden)
• Geoff Sutcliffe (University of Miami, USA)
• Josef Urban (Radboud University, NL)