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

(Continue reading)

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.

(Continue reading)

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

(Continue reading)

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.
(Continue reading)

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:
(Continue reading)

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
(Continue reading)

PAUL WARREN | 2 Oct 12:42 2013

Fw: Use of ontology patterns

A number of you may have already completed my survey on ontology use, the results of which are available from my KMi webpage http://kmi.open.ac.uk/people/member/paul-warren.

I have prepared a follow-up survey to explore in more detail how people use ontology patterns.  The survey is available at: http://tinyurl.com/ontology-patterns.  

The survey will take only 15 minutes, although for the purposes of completeness it does repeat a few of the questions from the previous survey.

I would very much appreciate if you could spare a few minutes to answer this survey.  As before, all responses will be regarded as confidential and you will be sent a report of the survey's findings.

The survey will close in one week's time, i.e. on Wednesday 9th October.

Many thanks,

Paul Warren








Irene Celino | 5 Jul 10:43 2013
Picon

Final CfP - 2nd International Workshop on Ordering and Reasoning (OrdRing2013) <at> ISWC2013

[Apologies if you receive multiple copies of this call. Please redistribute
within your own group and among colleagues, thank you!]

[CALL FOR PAPERS]

2nd International Workshop on Ordering and Reasoning (OrdRing2013)
October 21st/22nd, 2013 - Sydney, Australia

Collocated with the 12th International Semantic Web Conference (ISWC 2013)

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

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

Abstract submission deadline: 10 July 2013 (extended deadline)
Paper submission deadline: 17 July 2013 (extended deadline)
Notification of acceptance: 9 August 2013

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

More and more applications require real-time processing of massive,
dynamically generated, ordered data; where order is often an essential
factor reflecting recency, proximity or relevance. Stream and
rank-aware data management techniques are progressively providing
reactive and reliable query answering over such massive datasets,
allowing integration of highly dynamic sources. Key to their success
is the use of streaming algorithms that harness the natural or
enforceable orders in the data. The expressive power of Semantic
technologies is needed in those applications, but Semantic
Technologies risk being unable to address the needs of those
applications, because they do not consider ordering as an essential
property. Ranking results is often seen as an “added task”, performed
after inference, without affecting the inference process, which is
order-agnostic.

However, we perceive a trend towards order-aware semantic
technologies: both researchers and practitioners understand that order
matters in reasoning over massive and highly dynamic data. The idea of
Stream Reasoning is gaining considerable momentum. Some top-k query
answering techniques for Linked Data appeared. Several works are
considering SPARQL query answering on RDF annotated with labels
partially ordered. The Description Logic community is investigating
top-k ontological query answering.

This workshop 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. We see this
workshop as a first step to stimulate and guide a paradigm shift in
semantic technologies.

Topics include, but not limited to:

 - Inferencing with streaming algorithms
 - Ontological query answering over highly dynamic data
 - Incremental maintenance of materialization of highly dynamic data
 - Ontological top-k query answering over massive ordered data
 - A top-k query answering for fuzzy logics
 - Continuous query answering for fuzzy logics
 - Knowledge Representation for ordered facts
 - Applications of stream reasoning and top-k ontological query answering
 - Role of parallelization and distribution in order-aware semantic technologies
 - Harvesting and combining orders in data
 - Approximation approaches to inference with orderings
 - Proposals for and applications of benchmarks
 - 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 demos
and posters not exceeding 4 pages, short position 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 OrdRing2013 web submission system
(http://www.easychair.org/conferences/?conf=ordring2013).

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

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

Emanuele Della Valle (Politecnico di Milano)
Markus Krötzsch (University of Oxford)
Stefan Schlobach (Vrije Universiteit Amsterdam)
Irene Celino (CEFRIEL)

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

* Alessandro Bozzon (Delft University of Technology)
* David Carral (Wright State University)
* Oscar Corcho (Universidad Politécnica de Madrid)
* Peter Haase (fluid Operations)
* Carsten Lutz (Universität Bremen)
* Jeff Z. Pan (University of Aberdeen)
* Axel Polleres (Siemens AG Österreich / DERI, National University of Ireland, Galway)
* Sebastian Rudolph (Technische Universität Dresden)
* Steffen Staab (University of Koblenz-Landau)
* Umberto Straccia (ISTI-CNR)
* Guido Vetere (IBM)
* Haofen Wang (Shanghai Jiao Tong University)
* Kewen Wang (Griffith University)
* Gerhard Weikum (Max-Planck Institute for Informatics)
* Zhe Wu (Oracle)



--

http://about.me/iricelino/

    " If you understand what you're doing,
           you're not learning anything. "
Irene Celino | 17 Jun 14:28 2013
Picon

2nd CfP - 2nd International Workshop on Ordering and Reasoning (OrdRing2013) <at> ISWC2013

[Apologies if you receive multiple copies of this call. Please redistribute
within your own group and among colleagues, thank you!]

[CALL FOR PAPERS]

2nd International Workshop on Ordering and Reasoning (OrdRing2013)
October 21st/22nd, 2013 - Sydney, Australia

Collocated with the 12th International Semantic Web Conference (ISWC 2013)

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

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

Abstract submission deadline: 3 July 2013
Paper submission deadline: 10 July 2013
Notification of acceptance: 9 August 2013

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

More and more applications require real-time processing of massive,
dynamically generated, ordered data; where order is often an essential
factor reflecting recency, proximity or relevance. Stream and
rank-aware data management techniques are progressively providing
reactive and reliable query answering over such massive datasets,
allowing integration of highly dynamic sources. Key to their success
is the use of streaming algorithms that harness the natural or
enforceable orders in the data. The expressive power of Semantic
technologies is needed in those applications, but Semantic
Technologies risk being unable to address the needs of those
applications, because they do not consider ordering as an essential
property. Ranking results is often seen as an “added task”, performed
after inference, without affecting the inference process, which is
order-agnostic.

However, we perceive a trend towards order-aware semantic
technologies: both researchers and practitioners understand that order
matters in reasoning over massive and highly dynamic data. The idea of
Stream Reasoning is gaining considerable momentum. Some top-k query
answering techniques for Linked Data appeared. Several works are
considering SPARQL query answering on RDF annotated with labels
partially ordered. The Description Logic community is investigating
top-k ontological query answering.

This workshop 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. We see this
workshop as a first step to stimulate and guide a paradigm shift in
semantic technologies.

Topics include, but not limited to:

 - Inferencing with streaming algorithms
 - Ontological query answering over highly dynamic data
 - Incremental maintenance of materialization of highly dynamic data
 - Ontological top-k query answering over massive ordered data
 - A top-k query answering for fuzzy logics
 - Continuous query answering for fuzzy logics
 - Knowledge Representation for ordered facts
 - Applications of stream reasoning and top-k ontological query answering
 - Role of parallelization and distribution in order-aware semantic technologies
 - Harvesting and combining orders in data
 - Approximation approaches to inference with orderings
 - Proposals for and applications of benchmarks
 - 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 demos
and posters not exceeding 4 pages, short position 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 OrdRing2013 web submission system
(http://www.easychair.org/conferences/?conf=ordring2013).

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

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

Emanuele Della Valle (Politecnico di Milano)
Markus Krötzsch (University of Oxford)
Stefan Schlobach (Vrije Universiteit Amsterdam)
Irene Celino (CEFRIEL)

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

* Alessandro Bozzon (Delft University of Technology)
* David Carral (Wright State University)
* Oscar Corcho (Universidad Politécnica de Madrid)
* Peter Haase (fluid Operations)
* Carsten Lutz (Universität Bremen)
* Jeff Z. Pan (University of Aberdeen)
* Axel Polleres (Siemens AG Österreich / DERI, National University of Ireland, Galway)
* Sebastian Rudolph (Technische Universität Dresden)
* Steffen Staab (University of Koblenz-Landau)
* Umberto Straccia (ISTI-CNR)
* Guido Vetere (IBM)
* Haofen Wang (Shanghai Jiao Tong University)
* Kewen Wang (Griffith University)
* Gerhard Weikum (Max-Planck Institute for Informatics)
* Zhe Wu (Oracle)



--

http://about.me/iricelino/

    " If you understand what you're doing,
           you're not learning anything. "
Christoph LANGE | 12 Jun 16:30 2013
Picon

CfP for Math. in Computer Science Special Issue on 'Enabling Domain Experts to use Formalised Reasoning' (deadline 31 Oct)

     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

Serge Autexier | 7 Jun 08:36 2013
Picon

Call for Participation CICM 2013 8-12 July 2013, Registration deadline 23rd June 2013


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

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

                     Call for participation 

                Registration deadline: 23 June 2013
-----------------------------------------------------------------------
Invited talks will be given by:

- Patrick Ion, Mathematical Reviews, American Mathematical Society, USA
- Assia Mahboubi, École Polytechnique and INRIA/Microsoft Research
  Joint Centre, France
- Ursula Martin, Queen Mary, University of London, UK

Co-Located Workshops:
- MathUI'13: Mathematical User Interfaces
- OpenMath Workshop 2013
- PLMMS'13: Programming Languages for Mechanized Mathematics Systems
- THedu'13: TP Components for Educational Software

The  global programme  of the  conference, tracks,  and  workshops are
available via:

http://cicm-conference.org/2013/cicm.php?event=&menu=detailed-programme

Accepted Papers:

- Pedro  Quaresma, Vanda  Santos  and Seifeddine  Bouallegue. The  Web
  Geometry Laboratory Project
- Russell  Bradford, James  H.  Davenport, Matthew  England and  David
  Wilson.  Optimising Problem  Formulation  for Cylindrical  Algebraic
  Decomposition
- Matthew  England, Russell  Bradford,  James H.  Davenport and  David
  Wilson. Understanding branch cuts of expressions
- Christoph Lange, Colin Rowat and Manfred Kerber. The ForMaRE Project
  - Formal Mathematical Reasoning in Economics
- Cezary Kaliszyk and Josef Urban. Automated Reasoning Service for HOL
  Light Corpora
- Jónathan Heras and  Ekaterina Komendantskaya. ML4PG: proof-mining in
  Coq
- Jónathan  Heras,  Gadea Mata,  Ana  Romero,  Julio  Rubio and  Rubén
  Sáenz.  Verifying  a  platform  for digital  imaging:  a  multi-tool
  strategy
- Dmitry  Chebukov, Alexandr  Izaak, Olga  Misurina, Yury  Pupyrev and
  Alexey Zhizhchenko. Math-Net.Ru as  a Digital Archive of the Russian
  Mathematical Knowledge
- Chau  Do  and Eric  Pauwels.  Using  MathML  to Represent  Units  of
  Measurement for Improved Ontology Alignment
- Miguel A. Abanades and Francisco Botana. A dynamic symbolic geometry
  environment for the computation of geometric loci and envelopes
- Shahab  Kamali and  Frank  Tompa. Structural  Similarity Search  For
  Mathematics Retrieval
- Rui  Hu   and  Stephen  Watt.  Determining   Points  on  Handwritten
  Mathematical Symbols
- Rein Prank. Software for  evaluating relevance of steps in algebraic
  transformations
- Eno  Tonisson. When  Students  Compare Their  Own  Answers with  the
  Answers of a Computer Algebra System
- Carst   Tankink,   Cezary   Kaliszyk,   Josef   Urban   and   Herman
  Geuvers. Formal Mathematics on Display: A Wiki for Flyspeck
- Michael Kohlhase, Felix Mance  and Florian Rabe. A Universal Machine
  for Biform Theory Graphs
- Florian Rabe. The MMT API: A Generic MKM System
- William  Farmer.  The  Formalization  of  Syntax-Based  Mathematical
  Algorithms Using Quotation and Evaluation
- Paul Libbrecht. Escaping the Trap of too Precise Topic Queries
- Bruno  Barras, Hugo  Herbelin, Lourdes  Del Carmen  González Huesca,
  Yann  Régis-Gianas,  Enrico  Tassi,  Makarius  Wenzel  and  Burkhart
  Wolff. Pervasive Parallelism in Highly-Trustable Interactive Theorem
  Proving Systems
- Christoph Lange,  Marco Caminati, Manfred  Kerber, Till Mossakowski,
  Colin Rowat, Makarius Wenzel and Wolfgang Windsteiger. A Qualitative
  Comparison  of the  Suitability of  Four Theorem  Provers  for Basic
  Auction Theory
- Deyan Ginev and Bruce Miller. LaTeXML 2012 - A Year of LaTeXML
- Xavier  Allamigeon,  Stéphane Gaubert,  Victor  Magron and  Benjamin
  Werner.  Certification  of   Bounds  of  Non-linear  Functions:  the
  Templates Method
- Bruce Miller. 3 Years of DLMF on the Web; Math & Search
- Minh-Quoc Nghiem,  Giovanni Yoko  Kristianto, Goran Topic  and Akiko
  Aizawa.  A  hybrid  approach   for  semantic  enrichment  of  MathML
  mathematical expressions
- Steven Obua,  Mark Adams and  David Aspinall. Capturing  Hiproofs in
  HOL Light
- Ulf Schöneberg  and Wolfram Sperber. Text analysis  in mathematics -
  the DeLiVerMATH project
- Sebastian Bönisch, Michael Brickenstein, Hagen Chrapary, Gert-Martin
  Greuel and Wolfram  Sperber. swMATH - a new  service for mathematics
  software
- Christoph Lüth  and Martin Ring.  A Web Interface for  Isabelle: The
  Next Generation
- Michal   Růžička,  Petr   Sojka  and   Vlastimil   Krejčíř.  Towards
  Machine-Actionable Modules of a Digital Mathematics Library

Registration is online via

http://cicm-conference.org/2013/cicm.php?event=&menu=registration


Gmane