The Coq mailing list

[Wolfgang Windsteiger <Wolfgang.Windsteiger AT risc.jku.at>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256

Dear colleagues,

At the 4th International Congress on Mathematical Software (which is a
satellite conference to the International Mathematical Congress) we
will organize a special session on

"Software for Mathematical Theory Exploration"  (and related topics),
see details below.

Please feel motivated and inspired to present a talk on your work
within this session.  Also, please, distribute this announcement to
other researchers who you think might be able to contribute to this event.

We look forward to receiving your extended abstract and to then
meeting you in Seoul.

Best regards and wishes,

Bruno Buchberger,  Session Organizer
Wolfgang Windsteiger,  Session Co-organizer.

- -- 
Dipl.-Ing. Dr. Wolfgang Windsteiger
RISC Institut / JKU Linz
Schloss Hagenberg, 4243 Hagenberg i.M., Austria
Phone: +43 732 2468-9960
http://www.risc.jku.at/home/wwindste/
PGP:
http://www.risc.jku.at/people/wwindste/Wolfgang_Windsteiger_at_risc_jku_at.asc
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.11 (GNU/Linux)
Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/

iF4EAREIAAYFAlMm+OAACgkQYOghb+jbC3bX2wEAllVirBCiVo0iWlS91lzxYmcs
G9IDkdoLCEWKRaRbbcAA/jBPC7B8qsTDdfgkwwo7xlV8EkkDYuEzxaKmpWqHx8gD
=2hh/
-----END PGP SIGNATURE-----
                      Call for Papers / Abstracts

                          ICMS 2014 Session
             Software for Mathematical Theory Exploration

        http://www.risc.jku.at/conferences/icms2014/MTE/MTE.html

                              as part of

        The 4th International Congress on Mathematical Software
                  Satellite Conference of ICM2014

                           August 5-9 2014
                  Hanyang University, Seoul, Korea


==========
Organizers
==========

Organizer: Bruno Buchberger
Co-Organizer: Wolfgang Windsteiger

Research Institute for Symbolic Computation (RISC)
Johannes Kepler University (JKU)
Schloss Hagenberg / Linz, Austria 

=====
Dates
=====

Abstract submission deadline:             March 31, 2014.
Extended Abstract submission deadline:    April 30, 2014.
Notification of acceptance:               May 15, 2014.
Workshop:                                 August 5-9, 2014.

=============
Aim and Scope
=============

In recent years, research groups all over the world have started to develop
software for supporting the process of exploring mathematical theories in a 
structured way. (Other names for this area are: mathematical knowledge 
management, formal mathematics.) Progress in this area is based on advances 
in 
automated reasoning and improvements in software and web technology.  

Research in this area has the potential to revolutionize the way how 
mathematical research, quality control in mathematics, archiving and 
dissemination of mathematical knowledge,  application of mathematics and 
education in mathematics will be done in the future.

======
Topics
======

This session is a forum for reporting on 
- new features and techniques in existing systems for mathematical theory
  exploration,
- new systems for mathematical theory exploration, or
- major case studies in mathematical theory exploration and its applications.

Examples of topics from these categories are
--------------------------------------------

- applications of theory exploration in mathematics education,
- development and assessment of tools for structuring large theories,
- graphical and organizational tools for visualization of theories
     and their dependencies,
- application of theory exploration in semantic web technologies,
- application of theory exploration in mathematical finance and economy,
- application of theory exploration in medical information systems,
- implications of theory exploration for the future of mathematical 
publishing,
- implications of theory exploration for archiving and quality
     control in mathematics,
- special reasoning techniques for special mathematical theories
     (e.g. inductive theories, set theory, computer algebra algorithms),
- application of theory exploration in software science (e.g. algorithm
      verification and/or synthesis),
- application of theory exploration for abstract sytate machine analysis,
- application of theory exploration in model checking,
- application of theory exploration in the development of
      Wolfram-Alpha-like web services,
- applications in math text book writing and preparing lecture notes,
- etc., etc.

===========
Publication
===========

- A short abstract will appear on the permanent conference web page 
  as soon as accepted.

- An extended abstract will appear on the permanent conference web page
  as soon as accepted. It will also appear on the proceedings that will be 
  distributed during the meeting.

- A special issue of the Journal of Symbolic Computation (JSC) consisting of
  full papers will be organized immediately after the meeting.

==========
Submission
==========

- If you would like to give a talk at ICMS, you need to submit first a short
  abstract and then later an extended abstract. See the guideline on the web
  for the details.

- After the meeting, the submission guidelines for a journal special issue 
will
  be communicated to you by the session organizers.