Modules and Libraries for Proof Assistants (MLPA-09)
This is the first workshop on module systems 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.
Goals of the workshop
- 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 of information retrieval, sharing, and management of change.
- Experience reports of industrial practitioners, using HOL, Isabelle/HOL, PVS, or other proof assistants.
Georges Gonthier INRIA Rocquencourt and Microsoft Research, Cambridge
|09:00 - 10:00||Combinatorics for Theorem Proving. Georges Gonthier. (Invited Talk)|
|10:00 - 10:30||Coffee Break|
|10:30 - 12:00||
|12:30 - 14:00||Catered Lunch|
|14:00 - 15:30||
|15:30 - 16:00||Coffee Break|
|16:00 - 18:00||Demo/discussion session, TBA|
|18:30 - 20:30||Reception at McCord Museum|
- 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
- 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