Apologies for duplicates.

      The ACM SIGSAM 2009 International Workshop on Programming
             Languages for Mechanized Mathematics Systems

                   Munich, Germany; August 21, 2009

   The ACM SIGSAM 2009 International Workshop on Programming Languages
   for Mechanized Mathematics Systems will be co-located with TPHOLs 2009.

   Registration for the PLMMS 2009 workshop is now open.

Important Dates and Deadlines

     * Abstract submission: Now closed
     * Submission deadline: Now closed
     * Author notification: June 22, 2009
     * Camera ready papers: July 15, 2009
     * Registration: Open, http://tphols.in.tum.de/fee.html
     * Workshop: August 21, 2009

General Information

   The scope of this workshop is at the intersection of programming
   languages and mechanized mathematics systems. The latter category
   subsumes present-day computer algebra systems, interactive proof
   assistants, and automated theorem provers, all heading towards
   fully integrated mechanized mathematical assistants.

Tentative Programme

Friday, August 21

   09:00-10:00 Invited talk (Session Chair:)
               Georges Gonthier. Ssreflect: Structured Scripting for
                                    Higher-Order Theorem Proving
   10:00-10:40 Coffee break

   10:40-12:10 Session 1 (Session Chair:)
               Paulo F. Silva, Joost Visser, Jose Oliveira. Galois: A
               Language for Proofs Using Galois Connections and Fork Algebras

               Makarius Wenzel. Parallel Proof Checking in Isabelle/Isar

               Andrea Asperti, Wilmer Riccioti, Claudio Sacerdoti
                         Coen, Enrico Tassi. A New Type for Tactics

   12:10-13:40 Lunch

   13:40-14:40 Invited tutorial (Session Chair:)

               Gabriel Dos Reis. OpenAxiom: A Categorial Platform for
                                    Scientific Computation

   14:40-15:10 Coffee Break

   15:10-16:10 Session 2 (Session Chair:)

               Joe Hurd. OpenTheory: Package Management for Higher
                            Order Logic Theories 

               Johannes Holzl. Proving Inequalities Over Reals With
                       Computation in Isabelle/HOL

   16:10-17:00 Business meeting

   Evening     Social Event


     * http://plmms09.cs.tamu.edu/, the PLMMS 2009 workshop web site
     * http://tphols.in.tum.de/, the THOPLs 2009 conference web site
     * http://tphols.in.tum.de/fee.html, registration site

Programme Committee

     * Clemens Ballarin, aicas GmbH
     * Gabriel Dos Reis, Texas A&M University (Co-Chair)
     * Jean-Christophe Filliâtre, CNRS Université Paris Sud
     * Predrag Janicic, University of Belgrade
     * Jaakko Järvi, Texas A&M University
     * Florina Piroi, Johannes Kepler University
     * Laurent Théry, INRIA Sophia Antipolis (Co-Chair)
     * Makarius Wenzel, Technische Universität München

Proofpower mailing list

Reply via email to