First call for papers: Module and Libraries for Proof Assistants
Florian Rabe <f.rabe <at> jacobs-university.de>
2009-02-06 23:32:54 GMT
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
------------------------------------------------------------------------------
Create and Deploy Rich Internet Apps outside the browser with Adobe(R)AIR(TM)
software. With Adobe AIR, Ajax developers can use existing skills and code to
build responsive, highly engaging applications that combine the power of local
resources and data with the reach of the web. Download the Adobe AIR SDK and
Ajax docs to start building applications today-http://p.sf.net/sfu/adobe-com
_______________________________________________
hol-info mailing list
hol-info <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
RSS Feed