[isabelle] First Call for Participation

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

              Munich, Germany
              August 21, 2009


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.


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


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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.