3rd Workshop on Modules and Libraries for Proof Assistants (MLPA-11)

joint with the 6th Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2011)
affiliated with the 2nd Conference on Interactive Theorem Proving (ITP 2011)
26 August 2011, Nijmegen

News

Description

MLPA-11 is the third workshop on module systems and libraries for proof assistants succeeding MLPA-09 at CADE and MLPA-10 at FLoC.

Goals

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.

Invited Speakers (of MLPA and LFMTP)

Programme

Programme Committee

Organization