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

Online Proceedings

An electronic copy of the proceedings is available here.

General Information

The scope of this workshop is at 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. Areas of interest include all aspects of PL and MMS that meet in the following topics, but not limited to:

This is the third PLMMS workshop; the first workshop was held with Calculemus 2007, the second held with CICM 2008.

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


Programme Committee