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.
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
The program committee welcomes submissions on all aspects of
programming languages and mechanised mathematics.
See the call for papers.
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
- 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?
only the programme on one page
||CTP-based program languages? Considerations about
an experimental design
||Florian Haftmann, Cezary Kaliszyk, and Walther Neuper
||Isabelle/ML vs. Isabelle/Scala
|Beluga: programming with contextual data, contexts, and ...
|The Abella Theorem Prover and Two-level Logic Reasoning
|Can we make Mathematics universal as well as fully reliable?
|| Pierre Cartier
transalpyne: a language for automatic transposition
|Luca De Feo and Eric Schost
||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
||The PIDE-Project : Towards multiple-sided, asynchronous Formal Documents
in the Isabelle/ISAR Framework
||Recent Developments in Omega's Proof Search
||Serge Autexier and Dominik Dietrich
- Jacques Carette -- Mechanized Mathematics
If one were designing an entirely new mathematical assistant, what might it look like? Problems and some favoured solutions are
[Joint invited talk with Calculemus; extended abstract (pdf)]
- Brigitte Pientka -- Beluga: programming with contextual data, contexts, and ...
The logical framework LF provides an elegant foundation for specifying
formal systems and proofs and it is used successfully in a
wide range of applications such as certifying code and mechanizing
meta-theory of programming languages. However, incorporating LF
technology into functional programming to allow programmers to specify
and reason about formal guarantees of their programs from within
the programming language itself has been a major challenge.
An overview of Beluga, will be presented. This is a framework for
programming and reasoning with formal systems. It supports specifying
formal systems in LF and it also provides a dependently typed
functional language that supports analyzing and manipulating LF data
via pattern matching. A distinct feature of Beluga is its direct
support for reasoning with contexts and contextual objects. Taken
together these features lead to powerful language which supports
writing compact and elegant proofs.
See the Beluga website for more information.
Andrew Gacek -- The Abella Theorem Prover and Two-level Logic Reasoning
The Abella theorem prover uses both a specification logic and a
reasoning logic. This two-level logic approach is particularly
fruitful in the domain of formalizing systems with binding structure.
In this talk, we discuss the structure and consequences of this
approach and explore possible extensions.
See the Abella website for more information.
Pierre Cartier -- Can we make Mathematics universal as well as fully reliable ?
[Joint invited talk with MKM]
These are times of change for the mathematical profession and for the practice of mathematics, with, for instance, the advent of powerful computing machinery and the extraordinary immediacy of communication all over the world. If the concept of globalization has any meaning, this is now the time of globalization in mathematics. The pretense of mathematics of being universal can now be made real, and mathematical knowledge be shared by people from many different background. In addition, there are now mechanical help in reasoning, digitization of large parts of the traditional mathematical literature, and amazing amounts of scientific data and problems begging analysis which all help to offer a change in the role of mathematics. Checking proofs by computers is just one of the many new possibilities. A new paradigm is needed to understand a world of TERABYTES, where the frontier between "proof" and "guess" is quite fuzzy. Between "finite" and "infinite", we have to introduce in our axiomatics the world of "very very large".
|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
|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|
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
Papers and demo proposals should be submitted via PLMMS 2010
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.
- Thorsten Altenkirch (University of Nottingham, UK)
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)