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
------------------------------------------------------------------------------
This SF.net email is sponsored by:
High Quality Requirements in a Collaborative Environment.
Download a free trial of Rational Requirements Composer Now!
http://p.sf.net/sfu/www-ibm-com
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
