MLPA-10: July 15

2nd Workshop on Module Systems and Libraries for Proof Assistants

associated with IJCAR and ITP


This is the second workshop on module systems and libraries for proof assistants succeeding MLPA-09, which was held during CADE-22. This year the program will consist only of invited talks.

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 workshop aims to attract and bring together researchers and practitioners with background and experience in the design, implementation, and application of module systems from different logic-based systems such as theorem provers, proof assistants, and programming languages. Because it is affiliated with both and takes place between ITP and IJCAR, the workshop will provide the fertile venue for the exchange of ideas and experiences.

More information can be found here.


Invited Talks

Program Chairs

Florian Rabe, Jacobs University Bremen, Germany
Carsten Schuermann, IT University of Copenhagen, Denmark

Program Committee:

Stefan Berghofer, Technische Universit√§t M√ľnchen, Germany
Derek Dreyer, Max Planck Institute for Software Systems, Germany
Georges Gonthier, Microsoft Research, United Kingdom
Zhaohui Luo, Dept of Computer Science, Royal Holloway, Univ of London, United Kingdom
Till Mossakowski, DFKI Lab Bremen, Germany
Scott Owens, University of Cambridge, United Kingdom