The Coq mailing list

[Florian Rabe <f.rabe AT jacobs-university.de>]

                   Call for Participation
                   First International Workshop on
          Modules and Libraries for Proof Assistants
                              (MLPA'09)
            http://www.itu.dk/~carsten/mlpa-09.html
                       August 3, 2009

                       Affiliated with CADE-22
                 Montreal, Canada, August 2-7, 2009

            EARLY REGISTRATION DEADLINE: June 30

MLPA'09 is the first international workshop on modules and libraries
for proof assistants. It brings 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.

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.

Program:

09:00 - 10:00   Invited Talk
  Georges Gonthier, Combinatorics for Theorem Proving
10:00 - 10:30   Coffee Break
10:30 - 12:00     Regular talks
  Zhaohui Luo, Dependent Record Types Revisited
  Elie Soubiran, A unified framework and a transparent name-space for the Coq 
module system.
  Hyeonseung Im and Sungwoo Park, A module system independent of base 
languages
12:30 - 14:00   Catered Lunch
14:00 - 15:30     Regular talks
  Nicolas Bertaux and David Delahaye, Developing and Managing Libraries using 
the Focal Environment
  Michael Franssen and Mark van den Brand, Design of a Proof Repository 
Architecture
  Stefania Dumbrava, Fulya Horozal and Kristina Sojakova, A Case Study on 
Formalizing Algebraic Structures in a Module System
15:30 - 16:00   Coffee Break
16:00 - 18:00   System demo and discussion session
18:30 - 20:30   CADE Reception at McCord Museum

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

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