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