[TYPES/announce] CfP PLMMS at CICM, July 2013, Bath, UK

[Iain Whiteside]

	(* Apologies for multiple copies *)

-------------------------------------------------------------------
                    CALL FOR PAPERS
-------------------------------------------------------------------
	    The 5th International Workshop on

Programming Languages for Mechanized Mathematics Systems
                                   (PLMMS 2013)

Part of CICM-2013, at University of Bath, UK 8-12th of July 2013
-------------------------------------------------------------------

Important Dates
---------------

* Abstract submission:              Mon May   6 2013
* Paper submission:                  Mon May  13 2013
* Notification of acceptance:    Mon June  3 2013
* Camera ready copy due:       Mon June 10 2013

Program Committee
-----------------

* David Aspinall, University of Edinburgh, UK
* Serge Autexier, DKFI Bremen, Germany
* Jacques Carette, McMaster University, Canada
* Claudio Sacerdoti Coen, University of Bologna, Italy
* Gudmund Grov, Heriot Watt University, UK
* Cezar Ionescu, Potsdam Institute, Germany
* Ewen Maclean, University of Edinburgh, UK
* Florian Rabe (co-chair), Jacobs University, Germany
* Tim Sheard, Portland State University, USA
* Sergei Soloviev, IRIT, France
* Stephen Watt, University of Western Ontario, Canada
* Makarius Wenzel, Université Paris-Sud, France
* Iain Whiteside (co-chair), University of Newcastle, UK
* Freek Wiedijk, Radboud University, Netherlands
* Wolfgang Windsteiger, RISC, Austria

PLMMS Scope
-----------

The program committee welcomes submissions on programming language
issues related to all aspects of mechanised mathematics systems
(MMS). In particular:

- Mathematical algorithms
- Tactics and proof search
- Proofs
- Mathematical notation

Of particular interest are the dimensions of:

- Expressiveness
- Efficiency
- Correctness
- Understandability and Usability
- Modularity and Extensibility
- Design and implementation

Mechanised mathematics systems, whether stand-alone or embedded in
larger systems, include but are not limited to:

- Dependent typed programming languages
- Proof assistants
- Computer algebra systems
- Proof planning systems
- Theorem proving systems
- Theory formation systems

These issues have a very colourful history. Why are all the languages
of mainstream computer algebra systems untyped?  Why are the (strongly
typed) proof assistants so much harder to use than a typical computer
algebra systems?  What forms of polymorphism exist in mathematics?
What forms of dependent types may be used in mathematical modelling?
How can MMS regain the upper hand on issues of "genericity" and
"modularity"?  What are the biggest barriers when using more
mainstream languages for computer algebra systems, proof assistants or
theorems provers?

Many programming language innovations appeared in either computer
algebra or proof systems first, before migrating into more mainstream
programming languages.  This workshop is an opportunity to present the
latest innovations in the design of MMS that may be relevant to future
programming languages, or conversely novel programming language
principles that improve upon the implementation and deployment of MMS.


Submission Details
------------------

Papers should be submitted via the PLMMS 2013 easychair website:

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

Submissions must describe original unpublished work which is not been
submitted for publication elsewhere. At least one author of each
accepted paper is expected to attend PLMMS 2013 and present her or his
paper.

We wish to be flexible with paper length and will accept papers between
4 and 15 pages in length, submitted in PDF format. We invite submissions
of both work-in-progress and fully polished research.

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.com/computer/lncs/lncs+authors

Papers will be reviewed by at least three reviewers. Informal workshop 
proceeding will be circulated as a technical report and on CEUR-WS.


Links
-----

* https://www.easychair.org/conferences/?conf=plmms2013
 abstract and paper submission webpage

* http://www.springer.com/computer/lncs/lncs+authors
 submission style guide

* http://www.cicm-conference.org/2013/cicm.php?event=plmms&menu=general
 the PLMMS 2013 web site

* http://www.cicm-conference.org/2013/cicm.php
 the CICM 2013 conference web site
-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.