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: August 2, 2009
Workshop: August 21, 2009

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:

Dedicated input languages for MMS: covers all aspects of languages intended for the user to deploy or extend the system, both algorithmic and declarative ones. Typical examples are tactic definition languages such as Ltac in Coq, mathematical proof languages as in Mizar or Isar, or specialized programming languages built into CA systems.
Mathematical modeling languages used for programming: covers the relation of logical descriptions vs. algorithmic content. For instance the logic of ACL2 extends a version of Lisp, that of Coq is close to Haskell, and some portions of HOL are similar to ML and Haskell, while Maple tries to do both simultaneously. Such mathematical languages offer rich specification capabilities, which are rarely available in regular programming languages. How can programming benefit from mathematical concepts, without limiting mathematics to the computational worldview?
Programming languages with mathematical specifications: covers advanced mathematical concepts in programming languages that improve the expressive power of functional specifications, type systems, module systems etc. Programming languages with dependent types are of particular interest here, as is intentionality vs extensionality.
Language elements for program verification: covers specific means built into a language to facilitate correctness proofs using MMS. For example, logical annotations within programs may be turned into verification conditions to be solved in a proof assistant eventually. How need MMS and PL to be improved to make this work conveniently and in a mathematically appealing way?

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

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