[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS] First call for papers: Module and Libraries for Proof Assistants

		   First International Workshop on
	  Modules and Libraries for Proof Assistants

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



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

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


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:

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.


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