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 Links * 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 Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com