Modules and Libraries for Proof Assistants (MLPA-10)

15 July 2010, Edinburgh
affiliated with IJCAR and ITP as part of FLoC


This was the second workshop on module systems and libraries for proof assistants succeeding MLPA-09, which was held during CADE-22. It was held at FLoC.

The program consisted only of invited talks: Collection of abstracts in pdf format.


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 and has the potential to impact the way we organize proofs and programs in the future.


Program Committee