PLMMS 2010
Programming Languages for Mechanized Mathematics Systems
The 2009 International Workshop on Programming Languages for
Mechanized Mathematics Systems is an ACM SIGSAM
in-coorperation workshop, co-located
with CICM 2010
8th July 2010 at CNAM, Paris.
Overview:
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. The program committee welcomes submissions on all aspects of programming
languages and mechanised mathematics that meet, but not limited to, the following
topics:
- 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 modeling 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?
Important Dates:
| 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 |
Submissions:
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.
Programme Committee:
- 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)
History: