The Coq mailing list

[Laurent Th�ry <Laurent.Thery AT sophia.inria.fr>]

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

              Munich, Germany
              August 21, 2009

           FIRST CALL FOR PARTICIPATION

            http://plmms09.cse.tamu.edu/


The ACM SIGSAM PLMMS 2009 international workshop will be co-located with
TPHOLs 2009.

This workshop is focused on the intersection of programming languages
(PL) and mechanized mathematics systems (MMS). The latter category
subsumes present-day computer algebra systems (CAS), interactive proof
assistants (PA), and automated theorem provers (ATP), all heading
towards fully integrated mechanized mathematical assistants that are
expected to emerge eventually.


PRELIMINARY 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


Links

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