[Om-announce] Last call for papers: Modules and Libraries for Proof Assistants (CADE workshop)

[Florian Rabe]

		   First International Workshop on
	  Modules and Libraries for Proof Assistants
			      (MLPA'09)
	    http://www.itu.dk/~carsten/mlpa-09.html

		       Affiliated with CADE-22
		 Montreal, Canada, August 2-7, 2009

			   CALL FOR PAPERS

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

Important Dates:

Abstract Submission     27 April  2009
Submission deadline:     4 May    2009
Author Notification:     8 June   2009
Final Version:           6 July   2009
Workshop day             3 August 2009

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

MLPA'09 is the first international workshop on modules and libraries
for proof assistants.

Over the last twenty years, users of proof assistants and automated
theorem provers have created large libraries of formal proofs and
mathematical knowledge.  Module systems help with the tedious tasks of
organizing, sharing, and maintaining libraries.  In the view of the
ever increasing complexity of this network of information, module
systems offer many of the answers to the practical problems that proof
assistant system developers face today and can therefore be seen as an
emerging research for the automated deduction community.

The proposed workshop aims to attract and bring together researchers
and practitioners with background and experience in module systems from
different logic based systems, such as theorem provers, proof
assistants, and programming languages.  Because it is affiliated with
CADE, the workshop will provide the fertile venue for the exchange of
ideas and experiences and has the potential to impact the way we organize
proofs and programs in the future.

The broad aim of the proposed workshop is to run a short, but highly
focused meeting, which will provide researchers with a forum to review
state-of-the-art results and techniques, from theory to practice of
module systems and to present recent and new progress in:

* The design of module systems for programming languages and proof
  systems.

* The implementation of formal digital libraries.

* System descriptions of existing module systems, for example ML
  modules, type classes, Coq's, or Agda's module system.

* Case studies regarding information retrieval, sharing, and
  management of change.

* Experience reports of industrial practitioners, using HOL,
  Isabell/HOL, PVS, or other proof assistants.

Program Committee:

    * Stefan Berghofer, Technische Universität München, Germany
    * Derek Dreyer, MPI-SWS, Saarbruecken, Germany
    * Hugo Herbelin, INRIA, France
    * Conor McBride, University of Nottingham, Great Britain
    * Till Mossakowski, German Research Center for Artificial Intelligence
    * Ulf Norell, Chalmers University, Sweden
    * Randy Pollack, University of Edinburgh, Great Britain
    * Florian Rabe, Jacobs University, Bremen, Germany
    * Carsten Schuermann, IT University of Copenhagen, Denmark

Paper Submissions:

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

Three categories of papers are solicited:

* Category A: Detailed and technical accounts of new research: up to
  fifteen pages including bibliography.

* Category B: Shorter accounts of work in progress and proposed
  further directions, including discussion papers: up to eight pages
  including bibliography and appendices.

* Category C: System descriptions presenting an implemented tool and
  its novel features: up to six pages. A demonstration is expected to
  accompany the presentation.

Submission is electronic in postscript or PDF format. Submitted papers
must conform to the ENTCS style preferrably using LaTeX2e. For further
information and submission instructions, see the MLPA web page:
http://www.itu.dk/~carsten/mlpa-09.html

Proceedings are to be published as a volume in the Electronic Notes in
Theoretical Computer Science (ENTCS) series and will be available to
participants at the workshop.

Authors of accepted papers are expected to present their paper at
the workshop.

Organizers:

Florian Rabe                        Carsten Schuermann
f.rabe at jacobs-university.de      carsten at itu.dk
Jacobs University                   IT University of Copenhagen
Bremen, Germany		      	Copenhagen, Denmark