[Agda] Call for Participation: Modules and Libraries for Proof Assistants (CADE workshop)

[Florian Rabe]

                   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