PLMMS 2010

Programming Languages for Mechanized Mathematics Systems

The 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems is co-located with CICM 2010

8th July 2010 at CNAM, Paris.

The programme chairs are James Davenport and Lucas Dixon.

NEWS: You can now register for participation (via CICM).


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:


only the programme on one page

[Invited Talk]
Mechanized Mathematics Jacques Carette
09:35--10:05 CTP-based program languages? Considerations about an experimental design Florian Haftmann, Cezary Kaliszyk, and Walther Neuper
10:05--10:30 Isabelle/ML vs. Isabelle/Scala Makarius Wenzel
10:30-11:00 COFFEE BREAK
[Invited Talk]
Beluga: programming with contextual data, contexts, and ... Brigitte Pientka
[Invited Talk]
The Abella Theorem Prover and Two-level Logic Reasoning Andrew Gacek
12:30--14:00 LUNCH
[Invited Talk]
Can we make Mathematics universal as well as fully reliable? Pierre Cartier
15:05--15:35 transalpyne: a language for automatic transposition Luca De Feo and Eric Schost
15:35--16:05 LEMA: Towards a language for reliable arithmetic Vincent Lefèvre, Philippe Théveny, Florent de Dinechin, Claude-Pierre Jeannerod, Christophe Mouilleron, David Pfannholzer, Nathalie Revol
16:05--16:30 The PIDE-Project : Towards multiple-sided, asynchronous Formal Documents in the Isabelle/ISAR Framework Burkhart Wolff
14:30--17:00 COFFEE BREAK
17:00--17:30 Recent Developments in Omega's Proof Search Programming Language Serge Autexier and Dominik Dietrich

Invited Talks:

Important Dates:

Abstract submission:Tue 6 April 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
Submission of demo and presentation proposals:Mon 17 May 2010 (by PLMMS 2010 easychair)
Notification of acceptance:Mon 24 May 2010
Camera ready copy due:Mon 7 June 2010
Workshop:Thu 8 July 2010

Submissions: (See the call for papers)

We welcome submission of proposals to present a demo, as well as submissions of papers presenting original unpublished work which is not been submitted for publication elsewhere.

Selected papers will appear in the ACM Communications in Computer Algebra. All accepted papers and system demos will be presented at the workshop, and the extended abstracts will be made available online.

Papers and demo proposals 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.

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

Programme Committee:


The 2009 PLMMS workshop, Munich, Germany. With TPHOLs

The 2008 PLMMS workshop, Birmingham, UK. With CICM

The 2007 PLMMS workshop, Hagenberg, Austria. With Calculemus