coq-club AT inria.fr
Subject: The Coq mailing list
List archive
[Coq-Club] Call for Participation: Modules and Libraries for Proof Assistants (CADE workshop)
chronological Thread
- From: Florian Rabe <f.rabe AT jacobs-university.de>
- To: ai AT cs.man.ac.uk, aiia AT di.unito.it, asl AT vassar.edu, concurrency AT cwi.nl, fm-discussion AT cs.man.ac.uk, arw-committee AT csc.liv.ac.uk, img AT cs.man.ac.uk, kr AT kr.org, lics AT informatik.hu-berlin.de, loginf AT lat.inf.tu-dresden.de, om-announce AT openmath.org, types-announce AT lists.seas.upenn.edu, pvs AT csl.sri.com, kgs-list AT logic.at, loco AT csc.liv.ac.uk, agents AT csc.liv.ac.uk, ki-inf AT uni-koblenz.de, newsletter AT aarinc.org, relmics-l AT McMaster.CA, theorem-provers AT ai.mit.edu, theory-logic AT cs.cmu.edu, elsnet-list AT let.uu.nl, math.logik AT gmx.net, twelf-list AT twelf.org, isabelle-users AT cl.cam.ac.uk, hol-info AT lists.sourceforge.net, coq-club AT pauillac.inria.fr, agda AT lists.chalmers.se, projects-mkm-ig AT jacobs-university.de
- Subject: [Coq-Club] Call for Participation: Modules and Libraries for Proof Assistants (CADE workshop)
- Date: Thu, 25 Jun 2009 02:39:07 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
- [Coq-Club] Call for Participation: Modules and Libraries for Proof Assistants (CADE workshop), Florian Rabe
Archive powered by MhonArc 2.6.16.