Oscar Corcho | 8 Jul 23:10 2014
Picon
Picon

OrdRing2014 deadline extension (July 14th)

[apologies for cross-posting]

3rd International Workshop on Ordering and Reasoning (OrdRing2014)
October 19th/20th, 2014 - Riva del Garda, Trentino, Italy

Co-located with the 13th International Semantic Web Conference (ISWC 2014)

http://www.streamreasoning.org/events/ordring2014

NEWS
---------------
* Deadline Extended to 14.7.2014
* The two best papers of OrdRing2014 have the opportunity to be published
on Journal on Data Semantics.

IMPORTANT DATES
---------------

Abstract submission deadline: still open
Paper submission deadline: July 14, 2014
Notification of acceptance: July 30, 2014

GOALS AND TOPICS
----------------

More and more applications require real-time processing of large,
dynamically generated, ordered data, where order captures essential
information about recency, proximity or relevance. Recency is crucial for
recognizing temporal events, as in complex event processing; proximity and
relevance are essential for ranking query answers, as in top-k query
(Continue reading)

Irene Celino | 18 Jun 11:12 2014
Picon

2nd CfP - 3rd International Workshop on Ordering and Reasoning - Riva del Garda, Italy, 19-20 October

[apologies for cross-posting]

3rd International Workshop on Ordering and Reasoning (OrdRing2014)
October 19th/20th, 2014 - Riva del Garda, Trentino, Italy

Co-located with the 13th International Semantic Web Conference (ISWC 2014)

http://www.streamreasoning.org/events/ordring2014

NEWS
---------------
The two best papers of OrdRing2014 have the opportunity to be published on Journal on Data Semantics.

IMPORTANT DATES
---------------

Abstract submission deadline: July 4, 2014
Paper submission deadline: July 11, 2014
Notification of acceptance: July 30, 2014

GOALS AND TOPICS
----------------

More and more applications require real-time processing of large, dynamically generated, ordered data, where order captures essential information about recency, proximity or relevance. Recency is crucial for recognizing temporal events, as in complex event processing; proximity and relevance are essential for ranking query answers, as in top-k query answering. In some cases, orders are a natural, even unavoidable, aspect of the data, which may constrain the ways in which we can access it. In other cases, orders need to be derived by additional computations, and then be enforced on the (unordered) input. While each of these scenarios represents some unique challenges, all of them involve streams of data and require us to reason about sequences of events. The goal of this workshop is to explore this joint concept of ordered data processing.

Semantic technologies can play a relevant role in this setting, as they provide the expressive power to integrate highly dynamic sources. This is also witnessed by a number of recent works on order-related concepts, such as Stream Reasoning and top-k ontological query answering. Stream and rank-aware data management techniques are progressively providing reactive and reliable query answering over massive datasets, while ontological process models allow us to define meaningful patterns in event streams. Related works range from applied topics, such as query optimization, to foundational topics, such as temporal logics.

This workshop (as its predecessors in 2011 and 2013) aims at bringing together this growing and very active community interested in integrating ordering with reasoning by using methods inspired by stream and rank-aware data management. It thus aims to stimulate and guide a paradigm shift in semantic technologies.

Topics include, but are not limited to:

- Streaming algorithms in query answering and reasoning
- Ontology-based data access over data streams
- Modelling complex events, processes, and patterns in ordered data
- Incremental maintenance of materialization of data streams
- Continuous query answering
- Ontological top-k query answering
- Continuous and top-k query answering for fuzzy and probabilistic logics
- Order in knowledge representation, such as temporal or spacial orders
- Topologies for distributed processing of data streams
- Data compression algorithms for data stream processing
- Parallelization and distribution in order-aware semantic technologies
- Approximation approaches to inference with orderings
- APIs for data stream exchange
- Proposals for and applications of benchmarks
- Applications of stream reasoning and top-k ontological query answering
- Implementation and evaluation experiences

SUBMISSION GUIDELINES AND PROCEEDINGS
-------------------------------------

We will welcome submissions describing ideas, experiments, and application visions originating from requirements for, and efforts aimed at, interleaving ordering and reasoning. We will encourage short position and short demo papers not exceeding 6 pages as well as longer technical papers not exceeding 12 pages. They should follow the LNCS proceedings style files..

Submissions should be formatted according to the Lecture Notes in Computer Science guidelines for proceedings available at http://www.springer.com/computer/lncs?SGWID=0-164-7-72376-0. Papers should be submitted in PDF format. All submissions will be done electronically via the OrdRing2014 web submission system (http://www.easychair.org/conferences/?conf=ordring2014).

At least one author of each accepted paper must register for the workshop. Information about registration will appear soon on the ISWC 2014 Web page.

The Workshop Proceedings will be published as CEUR Workshop Proceedings (www.ceur-ws.org)

ORGANISING COMMITTEE
--------------------

 * Irene Celino (CEFRIEL)
 * Oscar Corcho (Universidad Politécnica de Madrid)
 * Emanuele Della Valle (Politecnico di Milano)
 * Daniele Dell'Aglio (Politecnico di Milano)
 * Markus Krötzsch (Technische Universität Dresden)
 * Stefan Schlobach (Vrije Universiteit Amsterdam)


PROGRAM COMMITTEE
-----------------

Alessandro Bozzon (TU Delft)
Jean-Paul Calbimonte (École Polytechnique Fédérale de Lausanne)
Peter Haase (fluid Operations)
Alejandro Llaves (Universidad Politécnica de Madrid)
Carsten Lutz (University of Bremen)
Alessandro Margara (University of Lugano)
Tomas Masopust (TU Dresden)
Jeff Z. Pan (University of Aberdeen)
Giuseppe Pirrò (University of Koblenz-Landau)
Axel Polleres (WU Wien)
Umberto Straccia (ISTI-CNR)
Anni-Yasmin Turhan (TU Dresden)
Kewen Wang (Griffith University)
Zhe Wu (Griffith University)


--

http://about.me/iricelino/

    " If you understand what you're doing,
           you're not learning anything. "
Irene Celino | 19 May 15:08 2014
Picon

CfP - 3rd International Workshop on Ordering and Reasoning - Riva del Garda, Italy, 19-20 October

[apologies for cross-posting]

3rd International Workshop on Ordering and Reasoning (OrdRing2014)
October 19th/20th, 2014 - Riva del Garda, Trentino, Italy

Co-located with the 13th International Semantic Web Conference (ISWC 2014)

http://www.streamreasoning.org/events/ordring2014

IMPORTANT DATES
---------------

Abstract submission deadline: July 4, 2014
Paper submission deadline: July 11, 2014
Notification of acceptance: July 30, 2014

GOALS AND TOPICS
----------------

More and more applications require real-time processing of large, dynamically generated, ordered data, where order captures essential information about recency, proximity or relevance. Recency is crucial for recognizing temporal events, as in complex event processing; proximity and relevance are essential for ranking query answers, as in top-k query answering. In some cases, orders are a natural, even unavoidable, aspect of the data, which may constrain the ways in which we can access it. In other cases, orders need to be derived by additional computations, and then be enforced on the (unordered) input. While each of these scenarios represents some unique challenges, all of them involve streams of data and require us to reason about sequences of events. The goal of this workshop is to explore this joint concept of ordered data processing.

Semantic technologies can play a relevant role in this setting, as they provide the expressive power to integrate highly dynamic sources. This is also witnessed by a number of recent works on order-related concepts, such as Stream Reasoning and top-k ontological query answering. Stream and rank-aware data management techniques are progressively providing reactive and reliable query answering over massive datasets, while ontological process models allow us to define meaningful patterns in event streams. Related works range from applied topics, such as query optimization, to foundational topics, such as temporal logics.

This workshop (as its predecessors in 2011 and 2013) aims at bringing together this growing and very active community interested in integrating ordering with reasoning by using methods inspired by stream and rank-aware data management. It thus aims to stimulate and guide a paradigm shift in semantic technologies.

Topics include, but are not limited to:

- Streaming algorithms in query answering and reasoning
- Ontology-based data access over data streams
- Modelling complex events, processes, and patterns in ordered data
- Incremental maintenance of materialization of data streams
- Continuous query answering
- Ontological top-k query answering
- Continuous and top-k query answering for fuzzy and probabilistic logics
- Order in knowledge representation, such as temporal or spacial orders
- Topologies for distributed processing of data streams
- Data compression algorithms for data stream processing
- Parallelization and distribution in order-aware semantic technologies
- Approximation approaches to inference with orderings
- APIs for data stream exchange
- Proposals for and applications of benchmarks
- Applications of stream reasoning and top-k ontological query answering
- Implementation and evaluation experiences

SUBMISSION GUIDELINES AND PROCEEDINGS
-------------------------------------

We will welcome submissions describing ideas, experiments, and application visions originating from requirements for, and efforts aimed at, interleaving ordering and reasoning. We will encourage short position and short demo papers not exceeding 6 pages as well as longer technical papers not exceeding 12 pages. They should follow the LNCS proceedings style files..

Submissions should be formatted according to the Lecture Notes in Computer Science guidelines for proceedings available at http://www.springer.com/computer/lncs?SGWID=0-164-7-72376-0. Papers should be submitted in PDF format. All submissions will be done electronically via the OrdRing2014 web submission system (http://www.easychair.org/conferences/?conf=ordring2014).

At least one author of each accepted paper must register for the workshop. Information about registration will appear soon on the ISWC 2014 Web page.

The Workshop Proceedings will be published as CEUR Workshop Proceedings (www.ceur-ws.org)

ORGANISING COMMITTEE
--------------------

 * Irene Celino (CEFRIEL)
 * Oscar Corcho (Universidad Politécnica de Madrid)
 * Emanuele Della Valle (Politecnico di Milano)
 * Daniele Dell'Aglio (Politecnico di Milano)
 * Markus Krötzsch (Technische Universität Dresden)
 * Stefan Schlobach (Vrije Universiteit Amsterdam)


PROGRAM COMMITTEE
-----------------

Alessandro Bozzon (TU Delft)
Jean-Paul Calbimonte (École Polytechnique Fédérale de Lausanne)
Peter Haase (fluid Operations)
Alejandro Llaves (Universidad Politécnica de Madrid)
Carsten Lutz (University of Bremen)
Alessandro Margara (University of Lugano)
Tomas Masopust (TU Dresden)
Jeff Z. Pan (University of Aberdeen)
Giuseppe Pirrò (University of Koblenz-Landau)
Axel Polleres (WU Wien)
Umberto Straccia (ISTI-CNR)
Anni-Yasmin Turhan (TU Dresden)
Kewen Wang (Griffith University)
Zhe Wu (Griffith University)


--

http://about.me/iricelino/

    " If you understand what you're doing,
           you're not learning anything. "
Serge Autexier | 5 May 08:32 2014
Picon

CICM 2014: Invited Speakers & Call for Work-in-Progress Papers, 1 June 2014

   CICM 2014 - Conferences on Intelligent Computer Mathematics
      7-11 July 2014 at the University of Coimbra, Portugal
               http://www.cicm-conference.org/2014

         * * *  Announcement of Invited Speakers  * * * 

 * * * Call for Work-in-Progress Papers -- Deadline June 1 * * *

----------------------------------------------------------------------

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.  CICM  2014 offers  a venue  to discuss  these areas  and their
synergy.

The conference will take place at the University of Coimbra, Portugal,
and consists of four tracks:

* Calculemus, Chair: James Davenport

* Digital Mathematical Libraries (DML), Chair: Petr Sojka

* Mathematical Knowledge Management (MKM), Chair: Josef Urban

* Systems and Projects, Chair: Alan Sexton

As  in previous  years, there  will be  a Doctoral  Programme for  the
mentoring of Doctoral students and several co-located workshops.

* MathUI 2014: Mathematical User Interfaces
* OpenMath Workshop 2014
* The Notion of Proof 2014
* ThEdu 2014: TP Components for Educational Software
* Doctoral Programme

All of these are now accepting contributions.  Please see the web site
for their calls for submissions.

The  overall  programme is  organised  by  the General  Program  Chair
Stephen Watt.

----------------------------------------------------------------------
                          CICM Invited Talks
----------------------------------------------------------------------

* Yves Bertot, INRIA
  A naive view of homotopy type theory and its relation to 
  the calculus of constructions	

* Jaime Carvalho e Silva, U Coimbra
  What international studies say about the importance and limitations
  of using computers to teach mathematics in secondary schools

* Antonio Leal Duarte, U Coimbra [Joint Speaker with ADG 2014]
  Teaching Tiles

* Herbert Van de Sompel, Los Alamos Natioanl Laboratory
  Towards robust hyperlinks for web-based scholarly communication	

* Eric Weisstein, Wolfram|Alpha
  Computable data, mathematics, and digital libraries 
  in Mathematica and Wolfram|Alpha

----------------------------------------------------------------------
                 Work-in-Progress Call-for-Papers
----------------------------------------------------------------------

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.   Papers may  be on any  CICM topic,
including those from Calculemus, DML, MKM and Systems and Projects.

Accepted work-in-progress  papers will be presented  at the conference
as  short   teaser  talks   and  as  posters.    The  work-in-progress
proceedings  will   be  published  digitally  in   the  CEUR  Workshop
Proceedings series (CEUR-WS.org).

WiP  papers  should  be  prepared in  LaTeX  and  formatted  according
Springer's  LNCS   series  (the  corresponding  style   files  can  be
downloaded     from    http://www.springer.de/comp/lncs/authors.html).
Papers should be between 5 and 10 pages in length.

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.

----------------------------------------------------------------------
                Work-in-Progress Submission Particulars
----------------------------------------------------------------------

WiP paper submission deadline        :    1 June 2014
WiP paper notification of acceptance :   15 June 2014
WiP Camera ready copies due          :   20 June 2014
Conference                           : 7-11 July 2014

Electronic submission is done through Easychair at

    https://www.easychair.org/conferences/?conf=cicm2014wip

Note that this is different from the main CICM submission page.

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

Calculemus   2014  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)

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.

Serge Autexier | 22 Apr 09:26 2014
Picon

CfP: 8th Verification Workshop (VERIFY 2014), Focus Theme: Verification Beyond IT Systems, extended deadline *May 5th, 2014*

[Apologies for cross posting, Deadline extended to *May 5th, 2014*]

                            CALL FOR PAPERS

         8th International Verification Workshop (VERIFY'14)
              in connection with IJCAR 2014 at FLoC 2014
                  July 23-24, 2014, Vienna, Austria

                       http://vsl2014.at/verify

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  workshop series aims  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 2014 edition of VERIFY aims for extending the verification methods
for processes implemented in hard-  and software to processes that may
well include computer-assistance, but have  a large part or a frequent
interaction  with non-computer-based  process  steps.  Hence the  2014
edition will run under the focus theme

                    Verification Beyond IT Systems

A  non-exclusive list of application areas  with these characteristics
are

       * Ambient assisted living
       * Intelligent home systems and processes
       * Business systems and processes
       * Production logistics systems and processes
       * Transportation logistics
       * Clinical processes
       * Social systems and processes (e.g., voting systems)

The scope of VERIFY includes topics such as

       * ATP techniques in verification
       * Case studies (specification & verification)
       * Combination of verification systems
       * Integration of ATPs and CASE-tools
       * Compositional & modular reasoning
       * Experience reports on using formal methods
       * Gaps between problems & techniques
       * Formal methods for fault tolerance
       * Information flow control security
       * Refinement & decomposition
       * Reliability of mobile computing
       * Reuse of specifications & proofs
       * Management of change
       * Safety-critical systems
       * Security models
       * Tool support for formal methods

Submissions are encouraged in one of the following two categories:

A. Regular  paper:  Submissions  in  this  category  should   describe
   previously unpublished  work (completed or in  progress), including
   descriptions of research, tools,  and applications.  Papers must be
   5-14  pages  long (in  EasyChair  style)  or  6-15 pages  long  (in
   Springer LNCS style).

B. Discussion  papers: Submissions  in this  category are  intended to
   initiate discussions and hence should address controversial issues,
   and may include  provocative statements. Papers must  be 3-14 pages
   long  (in EasyChair  style) or  3-15 pages  long (in  Springer LNCS
   style).

Important dates
   Abstract Submission Deadline:    May 5th, 2014 (extended)
   Paper Submission Deadline:       May 5th, 2014 (extended)
   Notification of acceptance:      May 20, 2014
   Final version due:               May 27, 2014
   Workshop date:                   July 23-24, 2014

Submission is via EasyChair:
   http://www.easychair.org/conferences/?conf=verify2014

Program Committee

 Serge Autexier (DFKI) - chair
 Bernhard Beckert (Karlsruhe Institute of Technology) - chair
 Wolfgang Ahrendt (Chalmers University of Technology)
 Juan Augusto (Middlesex University)
 Iliano Cervesato (Carnegie Mellon University)
 Jacques Fleuriot (University of Edinburgh)
 Marieke Huisman (University of Twente)
 Dieter Hutter (DFKI GmbH)
 Reiner Haehnle (Technical University of Darmstadt)
 Deepak Kapur (University of New Mexico)
 Gerwin Klein (NICTA and UNSW)
 Joe Leslie-Hurd (Intel Corporation)
 Fabio Martinelli (IIT-CNR)
 Catherine Meadows (NRL)
 Stephan Merz (INRIA Lorraine)
 Tobias Nipkow (TU Munich)
 Lawrence Paulson (University of Cambridge)
 Johann Schumann (SGT, Inc/NASA Ames)
 Kurt Stenzel (University of Augsburg)

Serge Autexier | 7 Apr 10:01 2014
Picon

2nd CfP, VERIFY 2014, 8th Verification Workshop, *Abstract Deadline April 17th, 2014*, Focus Theme: Verification Beyond IT Systems

[Apologies for cross posting]

                        SECOND CALL FOR PAPERS

         8th International Verification Workshop (VERIFY’14)
              in connection with IJCAR 2014 at FLoC 2014
                  July 23–24, 2014, Vienna, Austria

                       http://vsl2014.at/verify

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  workshop series aims  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 2014 edition of VERIFY aims for extending the verification methods
for processes implemented in hard-  and software to processes that may
well include computer-assistance, but have  a large part or a frequent
interaction  with non-computer-based  process  steps.  Hence the  2014
edition will run under the focus theme

                    Verification Beyond IT Systems

A  non-exclusive list of application areas  with these characteristics
are

       * Ambient assisted living
       * Intelligent home systems and processes
       * Business systems and processes
       * Production logistics systems and processes
       * Transportation logistics
       * Clinical processes
       * Social systems and processes (e.g., voting systems)

The scope of VERIFY includes topics such as

       * ATP techniques in verification
       * Case studies (specification & verification)
       * Combination of verification systems
       * Integration of ATPs and CASE-tools
       * Compositional & modular reasoning
       * Experience reports on using formal methods
       * Gaps between problems & techniques
       * Formal methods for fault tolerance
       * Information flow control security
       * Refinement & decomposition
       * Reliability of mobile computing
       * Reuse of specifications & proofs
       * Management of change
       * Safety-critical systems
       * Security models
       * Tool support for formal methods

Submissions are encouraged in one of the following two categories:

A. Regular  paper:  Submissions  in  this  category  should   describe
   previously unpublished  work (completed or in  progress), including
   descriptions of research, tools,  and applications.  Papers must be
   5-14  pages  long (in  EasyChair  style)  or  6-15 pages  long  (in
   Springer LNCS style).

B. Discussion  papers: Submissions  in this  category are  intended to
   initiate discussions and hence should address controversial issues,
   and may include  provocative statements. Papers must  be 3-14 pages
   long  (in EasyChair  style) or  3-15 pages  long (in  Springer LNCS
   style).

Important dates
   Abstract Submission Deadline:    April 17th, 2014
   Paper Submission Deadline:       April 25th, 2014
   Notification of acceptance:      May 20, 2014
   Final version due:               May 27, 2014
   Workshop date:                   July 23–24, 2014

Submission is via EasyChair:
   http://www.easychair.org/conferences/?conf=verify2014

Program Committee

 Serge Autexier (DFKI) - chair
 Bernhard Beckert (Karlsruhe Institute of Technology) - chair
 Wolfgang Ahrendt (Chalmers University of Technology)
 Juan Augusto (Middlesex University)
 Iliano Cervesato (Carnegie Mellon University)
 Jacques Fleuriot (University of Edinburgh)
 Marieke Huisman (University of Twente)
 Dieter Hutter (DFKI GmbH)
 Reiner Hähnle (Technical University of Darmstadt)
 Deepak Kapur (University of New Mexico)
 Gerwin Klein (NICTA and UNSW)
 Joe Leslie-Hurd (Intel Corporation)
 Fabio Martinelli (IIT-CNR)
 Catherine Meadows (NRL)
 Stephan Merz (INRIA Lorraine)
 Tobias Nipkow (TU München)
 Lawrence Paulson (University of Cambridge)
 Johann Schumann (SGT, Inc/NASA Ames)
 Kurt Stenzel (University of Augsburg)

Serge Autexier | 28 Feb 09:47 2014
Picon

CICM 2014: Extended Deadline March 14th, 2014

   CICM 2014 - Conferences on Intelligent Computer Mathematics
        July 7-11, 2014 at University of Coimbra, Portugal

             http://www.cicm-conference.org/2014

                     Call for Papers

          ** Extended Deadline: March 14th, 2014 **

-------------------------------------------------------------------
* Co-located Workshops *
- CCA'14: Workshop on Compact Computer Algebra 
  (organiser: Elena Smirnova)
- MathUI'14: Workshop on Mathematical User Interfaces 
  (organisers: Andrea Kohlhase, Paul Libbrecht)
- OpenMath Workshop (organisers: James Davenport, Michael Kohlhase)
- Workshop on The Notion of Proof 
  (organisers: Jesse Alama, Reinhard Kahle)
- ThEdu'14: Workshop on Theorem Provers Components for Educational 
  Software (organisers: Walther Neuper, Pedro Quaresma)
-------------------------------------------------------------------

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  (CICM)
offer a venue for discussing these areas and their synergy.

CICM has been held annually  as a joint meeting since 2008, colocating
related conferences  and workshops to advance work  in these subjects.
Previous meetings have been held in Birmingham (U.K. 2008), Grand Bend
(Canada  2009), Paris  (France 2010),  Bertinoro (Italy  2011), Bremen
(Germany 2012) and Bath (U.K. 2013).

This is  a call for papers  for CICM 2014,  which will be held  at the
University   of  Coimbra,   7-11   July  2014,   following  the   10th
International Workshop on Automated Deduction in Geometry.

The principal tracks of the conference will be:

  Calculemus (Symbolic Computation and Mechanised Reasoning)
  Chair: James Davenport

  DML (Digital Mathematical Libraries)
  Chair: Petr Sojka

  MKM (Mathematical Knowledge Management)
  Chair: Josef Urban

  Systems and Projects
  Chair: Alan Sexton

The local  arrangements will be coordinated by  the Local Arrangements
Chair,   Pedro  Quaresma  (U.  Coimbra,  Portugal),  and  the  overall
programme will be organised by the General Program Chair, Stephen Watt
(U. Western Ontario, Canada).

The proceedings of the conference will be published by 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
----------------------------------------------------------------

Conference submissions:

  Abstract submission (extended):      ** 14 March 2014 **
  Submission deadline (extended):      ** 14 March 2014 **
  Reviews sent to authors:                 4 April 2014
  Rebuttals due:                	   8 April 2014
  Notification of acceptance:   	  14 April 2014
  Camera ready copies due:      	  25 April 2014

Work in progress and Doctoral Programme submissions:

  Submission deadline:          28 April 2014
  (Doctoral: Abstract+CV) 
  Notification of acceptance:   19 May 2014
  Camera ready copies due:      26 May 2014

Conference:                     7-11  July 2014

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

================================================================
Track Calculemus: Symbolic Computation and Mechanised Reasoning
================================================================

Calculemus   2014  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.

================================================================
Track DML: Digital Mathematical Libraries
================================================================

Mathematicians  dream of  a digital  archive containing  all validated
mathematical literature ever published, reviewed, properly linked, 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  for the
fulfillment  of the  dream of  a global  digital  mathematical library
(DML).  Computer scientists (D) and  librarians of the 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, including
the  processing  of  mathematical  knowledge expressed  in  scientific
papers in natural languages:

* 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 markup
  languages
* 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
* Reports and experience from running existing DMLs

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

================================================================
Track 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)

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

Electronic submission is done through Easychair

http://www.easychair.org/conferences/?conf=cicm2014

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 descriptions  and projects descriptions should be  2-4 pages in
the LNCS style and should present

* newly developed systems,
* systems not previously been presented to the CICM community, or
* significant updates to existing systems.

Systems must either be  available for download or currently executable
by the general public as a web application.

Project presentations should describe

* projects that are new or about to start,
* ongoing projects that have not yet been presented to the CICM community or
* 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.

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.

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

Chair: David Wilson (University of Bath, UK)

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 through EasyChair:

* A  two-page  abstract  of   your  thesis  describing  your  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: 28 April 2014.

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

General chair: Stephen Watt (University of Western Ontario, Canada)

Calculemus track
        James Davenport, University of Bath, UK  (Chair)
        Matthew England, University Of Bath, UK,
        Dejan Jovanović, SRI, USA
        Laura Kovács, Chalmers University of Technology, Sweden
        Assia Mahboubi, INRIA, France
        Adam Naumowicz, Institute of Informatics, U. Bialystok, Poland
        Grant Passmore, U. Cambridge and U. Edinburgh, UK
        Florian Rabe, Jacobs University Bremen. Germany
        Claudio Sacerdoti Coen, University of Bologna, Italy
        Freek Wiedijk, Radboud University Nijmegen, Netherlands
        (Other invitations pending)

DML track
        Petr Sojka, Masaryk University, Brno, CZ  (Chair)
        Akiko Aizawa, NII, University of Tokyo, Japan
        Łukasz Bolikowski, ICM, University of Warsaw, Poland
        Thierry Bouche, Université Joseph Fourier, Grenoble, france
        Yannis Haralambous, Inst Mines-Télécom - Télécom Bretagne, France
        Janka Chlebíková, School of Computing, University of Portsmouth, UK
        Michael Kohlhase, Jacobs University Bremen, Germany
        Jiří Rákosník, Institute of Mathematics AS CR, CZ
        David Ruddy, Cornell University, USA
        Volker Sorge, University of Birmingham, UK
        Frank Tompa, University of Waterloo, Canada
        Richard Zanibbi, Rochester Institute of Technology, USA

MKM track
        Josef Urban, Radboud University Nijmegen, The Netherlands  (Chair)
        Rob Arthan, Queen Mary University of London, UK
        David Aspinall, Univerity of Edinburgh, UK
        Michael Beeson, San Jose State University, USA
        Claudio Sacerdoti Coen, University of Bologna, Italy
        Thomas Hales, University of Pittsburgh, USA
        Johan Jeuring, Open Universiteit Nederland and Universiteit Utrecht, NL
        Peter Jipsen, Chapman University, USA
        Cezary Kaliszyk, University of Innsbruck, Austria
        Michael Kohlhase, Jacobs University Bremen, Germany
        Christoph Lange, University of Birmingham, UK
        Paul Libbrecht, Weingarten University of Education, Germany
        Ursula Martin, Queen Mary University of London, UK
        Bruce Miller, NIST, USA
        Adam Naumowicz, University of Bialystok, Poland
        Florian Rabe, Jacobs University Bremen, Germany
        Alan Sexton, University of Birmingham, UK
        Enrico Tassi, INRIA, France
        Stephen Watt, University of Western Ontario, Canada
        Makarius Wenzel, Université Paris-Sud 11, France
        Freek Wiedijk, Radboud University Nijmegen, The Netherlands

Systems & Projects track
        Alan Sexton, University of Birmingham, UK  (Chair)
        Christoph Lange, University of Bonn, Germany
        Jesse Alama, Technical University of Vienna, Austria
        Rob Arthan, Queen Mary University of London, UK
        Deyan Ginev, Jacobs University Bremen, Germany
        Jónathan Heras, University of Dundee, Scotland
        Mateja Jamnik, University of Cambridge, UK
        Predrag Janičić, University of Belgrade, Serbia
        Christoph Lüth, DFKI and University of Bremen, Germany
        Bruce Miller, NIST, Gaithersburg, Maryland, USA
        Hendrik Tews, TU Dresden, Germany

Serge Autexier | 21 Feb 16:49 2014
Picon

First Call for Papers: 8th Verification Workshop (VERIFY 2014), Focus Theme: Verification Beyond IT Systems

[Apologies for cross posting]

                        FIRST CALL FOR PAPERS

         8th International Verification Workshop (VERIFY’14)
              in connection with IJCAR 2014 at FLoC 2014
                  July 23–24, 2014, Vienna, Austria

                       http://vsl2014.at/verify

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  workshop series aims  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 2014 edition of VERIFY aims for extending the verification methods
for processes implemented in hard-  and software to processes that may
well include computer-assistance, but have  a large part or a frequent
interaction  with non-computer-based  process  steps.  Hence the  2014
edition will run under the focus theme

                    Verification Beyond IT Systems

A  non-exclusive list of application areas  with these characteristics
are

       * Ambient assisted living
       * Intelligent home systems and processes
       * Business systems and processes
       * Production logistics systems and processes
       * Transportation logistics
       * Clinical processes
       * Social systems and processes (e.g., voting systems)

The scope of VERIFY includes topics such as

       * ATP techniques in verification
       * Case studies (specification & verification)
       * Combination of verification systems
       * Integration of ATPs and CASE-tools
       * Compositional & modular reasoning
       * Experience reports on using formal methods
       * Gaps between problems & techniques
       * Formal methods for fault tolerance
       * Information flow control security
       * Refinement & decomposition
       * Reliability of mobile computing
       * Reuse of specifications & proofs
       * Management of change
       * Safety-critical systems
       * Security models
       * Tool support for formal methods

Submissions are encouraged in one of the following two categories:

A. Regular  paper:  Submissions  in  this  category  should   describe
   previously unpublished  work (completed or in  progress), including
   descriptions of research, tools,  and applications.  Papers must be
   5-14  pages  long (in  EasyChair  style)  or  6-15 pages  long  (in
   Springer LNCS style).

B. Discussion  papers: Submissions  in this  category are  intended to
   initiate discussions and hence should address controversial issues,
   and may include  provocative statements. Papers must  be 3-14 pages
   long  (in EasyChair  style) or  3-15 pages  long (in  Springer LNCS
   style).

Important dates
   Abstract Submission Deadline:    April 17th, 2014
   Paper Submission Deadline:       April 25th, 2014
   Notification of acceptance:      May 20, 2014
   Final version due:               May 27, 2014
   Workshop date:                   July 23–24, 2014

Submission is via EasyChair:
   http://www.easychair.org/conferences/?conf=verify2014

Program Committee

 Serge Autexier (DFKI) - chair
 Bernhard Beckert (Karlsruhe Institute of Technology) - chair
 Wolfgang Ahrendt (Chalmers University of Technology)
 Juan Augusto (Middlesex University)
 Iliano Cervesato (Carnegie Mellon University)
 Jacques Fleuriot (University of Edinburgh)
 Marieke Huisman (University of Twente)
 Dieter Hutter (DFKI GmbH)
 Reiner Hähnle (Technical University of Darmstadt)
 Deepak Kapur (University of New Mexico)
 Gerwin Klein (NICTA and UNSW)
 Joe Leslie-Hurd (Intel Corporation)
 Fabio Martinelli (IIT-CNR)
 Catherine Meadows (NRL)
 Stephan Merz (INRIA Lorraine)
 Tobias Nipkow (TU München)
 Lawrence Paulson (University of Cambridge)
 Johann Schumann (SGT, Inc/NASA Ames)
 Kurt Stenzel (University of Augsburg)

Serge Autexier | 17 Feb 15:02 2014
Picon

2nd Call for Papers: Conf. Intelligent Computer Mathematics (CICM 2014)

   CICM 2014 - Conferences on Intelligent Computer Mathematics
        July 7-11, 2014 at University of Coimbra, Portugal

             http://www.cicm-conference.org/2014

                    Second Call for Papers

-------------------------------------------------------------------
* Co-located Workshops *
- CCA'14: Workshop on Compact Computer Algebra 
  (organiser: Elena Smirnova)
- MathUI'14: Workshop on Mathematical User Interfaces 
  (organisers: Andrea Kohlhase, Paul Libbrecht)
- OpenMath Workshop (organisers: James Davenport, Michael Kohlhase)
- Workshop on The Notion of Proof 
  (organisers: Jesse Alama, Reinhard Kahle)
- ThEdu'14: Workshop on Theorem Provers Components for Educational 
  Software (organisers: Walther Neuper, Pedro Quaresma)
-------------------------------------------------------------------

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  (CICM)
offer a venue for discussing these areas and their synergy.

CICM has been held annually  as a joint meeting since 2008, colocating
related conferences  and workshops to advance work  in these subjects.
Previous meetings have been held in Birmingham (U.K. 2008), Grand Bend
(Canada  2009), Paris  (France 2010),  Bertinoro (Italy  2011), Bremen
(Germany 2012) and Bath (U.K. 2013).

This is  a call for papers  for CICM 2014,  which will be held  at the
University   of  Coimbra,   7-11   July  2014,   following  the   10th
International Workshop on Automated Deduction in Geometry.

The principal tracks of the conference will be:

  Calculemus (Symbolic Computation and Mechanised Reasoning)
  Chair: James Davenport

  DML (Digital Mathematical Libraries)
  Chair: Petr Sojka

  MKM (Mathematical Knowledge Management)
  Chair: Josef Urban

  Systems and Projects
  Chair: Alan Sexton

The local  arrangements will be coordinated by  the Local Arrangements
Chair,   Pedro  Quaresma  (U.  Coimbra,  Portugal),  and  the  overall
programme will be organised by the General Program Chair, Stephen Watt
(U. Western Ontario, Canada).

The proceedings of the conference will be published by 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
----------------------------------------------------------------

Conference submissions:

  Abstract submission:          28 February 2014
  Submission deadline:          7 March 2014
  Reviews sent to authors:      4 April 2014
  Rebuttals due:                8 April 2014
  Notification of acceptance:   14 April 2014
  Camera ready copies due:      25 April 2014

Work in progress and Doctoral Programme submissions:

  Submission deadline:          28 April 2014
  (Doctoral: Abstract+CV) 
  Notification of acceptance:   19 May 2014
  Camera ready copies due:      26 May 2014

Conference:                     7-11  July 2014

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

================================================================
Track Calculemus: Symbolic Computation and Mechanised Reasoning
================================================================

Calculemus   2014  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.

================================================================
Track DML: Digital Mathematical Libraries
================================================================

Mathematicians  dream of  a digital  archive containing  all validated
mathematical literature ever published, reviewed, properly linked, 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  for the
fulfillment  of the  dream of  a global  digital  mathematical library
(DML).  Computer scientists (D) and  librarians of the 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, including
the  processing  of  mathematical  knowledge expressed  in  scientific
papers in natural languages:

* 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 markup
  languages
* 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
* Reports and experience from running existing DMLs

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

================================================================
Track 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)

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

Electronic submission is done through Easychair

http://www.easychair.org/conferences/?conf=cicm2014

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 descriptions  and projects descriptions should be  2-4 pages in
the LNCS style and should present

* newly developed systems,
* systems not previously been presented to the CICM community, or
* significant updates to existing systems.

Systems must either be  available for download or currently executable
by the general public as a web application.

Project presentations should describe

* projects that are new or about to start,
* ongoing projects that have not yet been presented to the CICM community or
* 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.

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.

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

Chair: David Wilson (University of Bath, UK)

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 through EasyChair:

* A  two-page  abstract  of   your  thesis  describing  your  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: 28 April 2014.

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

General chair: Stephen Watt (University of Western Ontario, Canada)

Calculemus track
        James Davenport, University of Bath, UK  (Chair)
        Matthew England, University Of Bath, UK,
        Dejan Jovanović, SRI, USA
        Laura Kovács, Chalmers University of Technology, Sweden
        Assia Mahboubi, INRIA, France
        Adam Naumowicz, Institute of Informatics, U. Bialystok, Poland
        Grant Passmore, U. Cambridge and U. Edinburgh, UK
        Florian Rabe, Jacobs University Bremen. Germany
        Claudio Sacerdoti Coen, University of Bologna, Italy
        Freek Wiedijk, Radboud University Nijmegen, Netherlands
        (Other invitations pending)

DML track
        Petr Sojka, Masaryk University, Brno, CZ  (Chair)
        Akiko Aizawa, NII, University of Tokyo, Japan
        Łukasz Bolikowski, ICM, University of Warsaw, Poland
        Thierry Bouche, Université Joseph Fourier, Grenoble, france
        Yannis Haralambous, Inst Mines-Télécom - Télécom Bretagne, France
        Janka Chlebíková, School of Computing, University of Portsmouth, UK
        Michael Kohlhase, Jacobs University Bremen, Germany
        Jiří Rákosník, Institute of Mathematics AS CR, CZ
        David Ruddy, Cornell University, USA
        Volker Sorge, University of Birmingham, UK
        Frank Tompa, University of Waterloo, Canada
        Richard Zanibbi, Rochester Institute of Technology, USA

MKM track
        Josef Urban, Radboud University Nijmegen, The Netherlands  (Chair)
        Rob Arthan, Queen Mary University of London, UK
        David Aspinall, Univerity of Edinburgh, UK
        Michael Beeson, San Jose State University, USA
        Claudio Sacerdoti Coen, University of Bologna, Italy
        Thomas Hales, University of Pittsburgh, USA
        Johan Jeuring, Open Universiteit Nederland and Universiteit Utrecht, NL
        Peter Jipsen, Chapman University, USA
        Cezary Kaliszyk, University of Innsbruck, Austria
        Michael Kohlhase, Jacobs University Bremen, Germany
        Christoph Lange, University of Birmingham, UK
        Paul Libbrecht, Weingarten University of Education, Germany
        Ursula Martin, Queen Mary University of London, UK
        Bruce Miller, NIST, USA
        Adam Naumowicz, University of Bialystok, Poland
        Florian Rabe, Jacobs University Bremen, Germany
        Alan Sexton, University of Birmingham, UK
        Enrico Tassi, INRIA, France
        Stephen Watt, University of Western Ontario, Canada
        Makarius Wenzel, Université Paris-Sud 11, France
        Freek Wiedijk, Radboud University Nijmegen, The Netherlands

Systems & Projects track
        Alan Sexton, University of Birmingham, UK  (Chair)
        Christoph Lange, University of Bonn, Germany
        Jesse Alama, Technical University of Vienna, Austria
        Rob Arthan, Queen Mary University of London, UK
        Deyan Ginev, Jacobs University Bremen, Germany
        Jónathan Heras, University of Dundee, Scotland
        Mateja Jamnik, University of Cambridge, UK
        Predrag Janičić, University of Belgrade, Serbia
        Christoph Lüth, DFKI and University of Bremen, Germany
        Bruce Miller, NIST, Gaithersburg, Maryland, USA
        Hendrik Tews, TU Dresden, Germany

Serge Autexier | 22 Nov 16:44 2013
Picon

First Call for Papers: Conf. Intelligent Computer Mathematics (CICM 2014)

[Apologies for multiple copies]

   CICM 2014 - Conferences on Intelligent Computer Mathematics
        July 7-11, 2014 at University of Coimbra, Portugal

             http://www.cicm-conference.org/2014

                    First 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  Conferences on  Intelligent  Computer Mathematics  (CICM)
offer a venue for discussing these areas and their synergy.

CICM has been held annually  as a joint meeting since 2008, colocating
related conferences  and workshops to advance work  in these subjects.
Previous meetings have been held in Birmingham (U.K. 2008), Grand Bend
(Canada  2009), Paris  (France 2010),  Bertinoro (Italy  2011), Bremen
(Germany 2012) and Bath (U.K. 2013).

This is  a call for papers  for CICM 2014,  which will be held  at the
University   of  Coimbra,   7-11   July  2014,   following  the   10th
International Workshop on Automated Deduction in Geometry.

The principal tracks of the conference will be:

  Calculemus (Symbolic Computation and Mechanised Reasoning)
  Chair: James Davenport

  DML (Digital Mathematical Libraries)
  Chair: Petr Sojka

  MKM (Mathematical Knowledge Management)
  Chair: Josef Urban

  Systems and Projects
  Chair: Alan Sexton

The local  arrangements will be coordinated by  the Local Arrangements
Chair,  Paedro  Quaresma  (U.  Coimbra,  Portugal),  and  the  overall
programme will be organised by the General Program Chair, Stephen Watt
(U. Western Ontario, Canada).

The proceedings of the conference will be published by 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
----------------------------------------------------------------

Conference submissions:

  Abstract submission:          28 February 2014
  Submission deadline:          7 March 2014
  Reviews sent to authors:      4 April 2014
  Rebuttals due:                8 April 2014
  Notification of acceptance:   14 April 2014
  Camera ready copies due:      25 April 2014

Work in progress and Doctoral Programme submissions:

  Submission deadline:          28 April 2014
  (Doctoral: Abstract+CV) 
  Notification of acceptance:   19 May 2014
  Camera ready copies due:      26 May 2014

Conference:                     7-11  July 2014

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

================================================================
Track Calculemus: Symbolic Computation and Mechanised Reasoning
================================================================

Calculemus   2014  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.

================================================================
Track DML: Digital Mathematical Libraries
================================================================

Mathematicians  dream of  a digital  archive containing  all validated
mathematical literature ever published, reviewed, properly linked, 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  for the
fulfillment  of the  dream of  a global  digital  mathematical library
(DML).  Computer scientists (D) and  librarians of the 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, including
the  processing  of  mathematical  knowledge expressed  in  scientific
papers in natural languages:

* 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 markup
  languages
* 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
* Reports and experience from running existing DMLs

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

================================================================
Track 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)

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

Electronic submission is done through Easychair

http://www.easychair.org/conferences/?conf=cicm2014

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 descriptions  and projects descriptions should be  2-4 pages in
the LNCS style and should present

* newly developed systems,
* systems not previously been presented to the CICM community, or
* significant updates to existing systems.

Systems must either be  available for download or currently executable
by the general public as a web application.

Project presentations should describe

* projects that are new or about to start,
* ongoing projects that have not yet been presented to the CICM community or
* 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.

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.

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

Chair: David Wilson (University of Bath, UK)

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 through EasyChair:

* A  two-page  abstract  of   your  thesis  describing  your  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: 28 April 2014.

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

General chair: Stephen Watt (University of Western Ontario, Canada)

Calculemus track
        James Davenport, University of Bath, UK  (Chair)
        Matthew England, University Of Bath, UK,
        Dejan Jovanović, SRI, USA
        Laura Kovács, Chalmers University of Technology, Sweden
        Assia Mahboubi, INRIA, France
        Adam Naumowicz, Institute of Informatics, U. Bialystok, Poland
        Grant Passmore, U. Cambridge and U. Edinburgh, UK
        Florian Rabe, Jacobs University Bremen. Germany
        Claudio Sacerdoti Coen, University of Bologna, Italy
        Freek Wiedijk, Radboud University Nijmegen, Netherlands
        (Other invitations pending)

DML track
        Petr Sojka, Masaryk University, Brno, CZ  (Chair)
        Akiko Aizawa, NII, University of Tokyo, Japan
        Łukasz Bolikowski, ICM, University of Warsaw, Poland
        Thierry Bouche, Université Joseph Fourier, Grenoble, france
        Yannis Haralambous, Inst Mines-Télécom - Télécom Bretagne, France
        Janka Chlebíková, School of Computing, University of Portsmouth, UK
        Michael Kohlhase, Jacobs University Bremen, Germany
        Jiří Rákosník, Institute of Mathematics AS CR, CZ
        David Ruddy, Cornell University, USA
        Volker Sorge, University of Birmingham, UK
        Frank Tompa, University of Waterloo, Canada
        Richard Zanibbi, Rochester Institute of Technology, USA

MKM track
        Josef Urban, Radboud University Nijmegen, The Netherlands  (Chair)
        Rob Arthan, Queen Mary University of London, UK
        David Aspinall, Univerity of Edinburgh, UK
        Michael Beeson, San Jose State University, USA
        Claudio Sacerdoti Coen, University of Bologna, Italy
        Thomas Hales, University of Pittsburgh, USA
        Johan Jeuring, Open Universiteit Nederland and Universiteit Utrecht, NL
        Peter Jipsen, Chapman University, USA
        Cezary Kaliszyk, University of Innsbruck, Austria
        Michael Kohlhase, Jacobs University Bremen, Germany
        Christoph Lange, University of Birmingham, UK
        Paul Libbrecht, Weingarten University of Education, Germany
        Ursula Martin, Queen Mary University of London, UK
        Bruce Miller, NIST, USA
        Adam Naumowicz, University of Bialystok, Poland
        Florian Rabe, Jacobs University Bremen, Germany
        Alan Sexton, University of Birmingham, UK
        Enrico Tassi, INRIA, France
        Stephen Watt, University of Western Ontario, Canada
        Makarius Wenzel, Université Paris-Sud 11, France
        Freek Wiedijk, Radboud University Nijmegen, The Netherlands

Systems & Projects track
        Alan Sexton, University of Birmingham, UK  (Chair)
        Christoph Lange, University of Bonn, Germany
        Jesse Alama, Technical University of Vienna, Austria
        Rob Arthan, Queen Mary University of London, UK
        Deyan Ginev, Jacobs University Bremen, Germany
        Jónathan Heras, University of Dundee, Scotland
        Mateja Jamnik, University of Cambridge, UK
        Predrag Janičić, University of Belgrade, Serbia
        Christoph Lüth, DFKI and University of Bremen, Germany
        Bruce Miller, NIST, Gaithersburg, Maryland, USA
        Hendrik Tews, TU Dresden, Germany

Christoph LANGE | 3 Oct 13:10 2013
Picon

2nd CfP (deadline 31 Oct) Math. in Comp. Sci. Special Issue 'Enabling Domain Experts to use Formalised Reasoning'

     Call for Papers for a Special Issue of MATHEMATICS IN COMPUTER SCIENCE

              ENABLING DOMAIN EXPERTS TO USE FORMALISED REASONING
       http://www.cs.bham.ac.uk/research/projects/formare/pubs/mcs-doform/

           Guest editors: Manfred Kerber, Christoph Lange, Colin Rowat

We invite high-quality original research papers to a special issue of
the Birkhäuser/Springer journal Mathematics in Computer Science on the
use of systems based on a formal, explicit, machine-verifiable
representation of knowledge in application domains such as economics,
engineering, health care, education. Examples include:

* problems from application domains, which could benefit from better
  verification and knowledge management facilities, and

* knowledge management and verification tools, which domain experts
  can use without a computer science background. (Read more about our
  topics of interest)

For further examples, please see the Symposium on Enabling Domain
Experts to use Formalised Reasoning
(http://www.cs.bham.ac.uk/research/projects/formare/events/aisb2013/)
held at the annual convention of the AISB (Society for the Study of
Artificial Intelligence and Simulation of Behaviour) in April 2013.

    Submission: 31 October 2013
    Notification: 15 December 2013
    Revised version due: 15 January 2014
    Final version due: 15 February 2014
    Publication (expected): April 2014

Topics of interest include but are not limited to:

* for domain experts: what problems in application domains could
  benefit from better verification and knowledge management
  facilities? Possible fields include:

  - Example 1 (economics): auctions, value-at-risk models, trading
    algorithms, market design

  - Example 2 (engineering): system interoperability, manufacturing
    processes, product classification

* for computer scientists: how to provide the right knowledge
  management and verification tools to domain experts without a
  computer science background?

  -  wikis and blogs for informal, semantic, semiformal, and formal
     mathematical knowledge;
  -  general techniques and tools for online collaborative mathematics;
  -  tools for collaboratively producing, presenting, publishing, and
     interacting with online mathematics;
  -  automation and human-computer interaction aspects of mathematical
wikis;
  -  ontologies and knowledge bases designed to support knowledge
     management and verification in application domains;
  -  practical experiences, usability aspects, feasibility studies;
  -  evaluation of existing tools and experiments;
  -  requirements, user scenarios and goals.

Submissions should be approximately 20 pages long, should follow
publishers' instructions and should be submitted via EasyChair.

Potential contributors may contact the guest editors
(doformmcs2014@...) to discuss the suitability of topics and
papers.

--

-- 
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ Intelligent Computer Mathematics, 8–12 July, Bath, UK.
  Early registration deadline 23 June; http://cicm-conference.org/2013/
→ Knowledge and Experience Management, 7-9 October, Bamberg, Germany.
  Submission until 1 July; http://minf.uni-bamberg.de/lwa2013/cfp/fgwm/
→ Modular Ontologies (WoMO), 15 September, Corunna, Spain.
  Submission until 5 July; http://www.iaoa.org/womo/2013.html


Gmane