PLMMS 2010

The scope of this workshop is 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.

The program committee welcomes submissions on all aspects of programming languages and mechanised mathematics.

See the call for papers.

The topics of interest meet at, but are not limited to, the following:

• Input languages for MMS: all aspects of languages for the user to deploy or extend the system, both algorithmic and declarative. Typical examples are tactic languages such as Ltac in Coq, mathematical proof languages as in Mizar or Isar, and specialized programming languages built into CA systems.
• Mathematical modelling languages used for programming: 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 and mathematical specifications: 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: 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 can MMS and PL be improved to make verification more convenient and mathematically appealing?

Jacques Carette:

(Title TBA)

Abstract submission:	Fri 26 March 2010
Paper submission:	Fri 9 April 2010 (by PLMMS 2010 easychair)
Reviews sent to authors:	Mon 10 May 2010
Author's rebuttal deadline:	Mon 17 May 2010
Notification of acceptance:	Mon 24 May 2010
Early registration for attendance (via CICM):	TBA
Camera ready copy due:	Mon 7 June 2010
Workshop:	Thu 8 July 2010

Accepted papers will appear in the ACM Digital Library.

Papers should be submitted via PLMMS 2010 easychair. Papers should be no more than 8 pages in length and are to be submitted in PDF format. They must conform to the ACM SIGPLAN style guidelines. Each submission must also adhere to SIGPLAN's republication policy. Submissions must describe original unpublished work which is not been submitted for publication elsewhere.

At least one author of each accepted paper is expected to attend PLMMS 2010 and presents her or his paper.

• Thorsten Altenkirch (University of Nottingham, UK)
• Serge Autexier (DFKI, Germany)
• David Delahaye (CNAM, Paris, France)
• James Davenport [PC co-chair] (University of Bath, UK)
• Lucas Dixon [PC co-chair] (University of Edinburgh, UK)
• Gudmund Grov (University of Edinburgh, UK)
• Ewen Maclean (University of Herriot Watt, UK)
• Dale Miller (INRIA, France)
• Gabriel Dos Reis (Texas A&M University, USA)
• Carsten Schuermann (IT University of Copenhagen, Denmark)
• Tim Sheard (Portland State University, USA)
• Sergei Soloviev (IRIT, Toulouse, France)
• Stephen Watt (The University of Western Ontario, Canada)
• Makarius Wenzel (ITU Munich, Germany)
• Freek Wiedijk (Radboud University Nijmegen, Netherlands)

The 2009 PLMMS workshop, Munich, Germany. With TPHOLs

The 2008 PLMMS workshop, Birmingham, UK. With CICM

The 2007 PLMMS workshop, Hagenberg, Austria. With Calculemus