MLPA-09

From PLSwiki

Jump to: navigation, search

Contents

Modules and Libraries for Proof Assistants (MLPA-09)

This is the first workshop on module systems and libraries for proof assistants.


Description

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 proposed workshop aims to attract and bring 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. Because it is affiliated with CADE, 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.


Goals of the workshop

  • The design of module systems for programming languages and proof systems.
  • The implementation of formal digital libraries.
  • System descriptions of existing module systems, for example ML modules, type classes, Coq's, or Agda's module system.
  • Case studies regarding of information retrieval, sharing, and management of change.
  • Experience reports of industrial practitioners, using HOL, Isabelle/HOL, PVS, or other proof assistants.

Invited Speaker

Georges Gonthier INRIA Rocquencourt and Microsoft Research, Cambridge


Program

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

Organization

Important Dates

  • Abstract Submission: 27 April 2009
  • Submission deadline: 4 May 2009
  • Author Notification: 8 June 2009
  • Final Version: 6 July 2009
  • Workshop day: 3 August 2009

CFP

Call for papers.

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
Retrieved from "http://www.itu.dk/research/pls/wiki/index.php/MLPA-09"
Personal tools