Programming Languages for Mechanized Mathematics Workshop

As part of Calculemus 2007
Hagenberg, Austria
June 29-30, 2007

[Shortcuts: dates, registration, invited talk and program]

The intent of this workshop is to examine more closely the intersection between programming languages and mechanized mathematics systems (MMS). By MMS, we understand computer algebra systems (CAS), [automated] theorem provers (TP/ATP), all heading towards the development of fully unified systems (the MMS), sometimes also called universal mathematical assistant systems (MAS) (see Calculemus 2007).

There are various ways in which these two subjects of programming languages and systems for mathematics meet:

We are interested in all these issues. We hope that a certain synergy will develop between those issues by having them explored in parallel.

These issues have a very colourful history. Many programming language innovations first appeared in either CASes or Proof Assistants, before migrating towards more mainstream languages. One can cite (in no particular order) type inference, dependent types, generics, term-rewriting, first-class types, first-class expressions, first-class modules, code extraction, and so on. However, a number of these innovations were never aggressively pursued by system builders, letting them instead be developped (slowly) by programming language researchers. Some, like type inference and generics have flourished. Others, like first-class types and first-class expressions, are not seemingly being researched by anyone.

We want to critically examine what has worked, and what has not. Why are all the current ``popular''1 computer algebra systems untyped? Why are the (strongly typed) proof assistants so much harder to use than a typical CAS? But also look at question like what forms of polymorphism exists in mathematics? What forms of dependent types exist in mathematics? How can MMS regain the upper hand on issues of 'genericity'? What are the biggest barriers to using a more mainstream language as a host language for a CAS or an ATP?

This workshop will accept two kinds of submissions: full research papers as well as position papers. Research papers should be nore more than 15 pages in length, and positions papers no more than 3 pages. Submission will be through EasyChair. An informal version of the proceedings will be available at the workshop, now available as RISC Technical Report no. 07-10. We are (still) looking into having the best papers completed into full papers and published as a special issue of a Journal (details to follow).

Important Dates

May 02, 2007: Submission Deadline
May 30, 2006: Notification
June 29-30, 2007: Workshop

Program Committee

Lennart Augustsson [Credit Suisse]
Wieb Bosma [Radboud University Nijmegen, Netherlands]
Jacques Carette (co-Chair) [McMaster University, Canada]
David Delahaye [CNAM, France]
Jean-Christophe Filliâtre [CNRS and Université de Paris-Sud, France]
John Harrison [Intel Corporation, USA]
Josef Urban [Charles University, Czech Republic]
Markus (Makarius) Wenzel [Technische Universität München, Germany]
Freek Wiedijk (co-Chair) [Radboud University Nijmegen, Netherlands]
Wolfgang Windsteiger [University of Linz, Austria]

Location and Registration

Location information can be found on the Calculemus web site. Registration is joint with Calculemus -- make sure to carefully follow the instructions!

Invited Talk

PML -- a new proof assistant by Christophe Raffalli (slides available)

ABSTRACT: We will present our ongoing work on a new proof assistant and deduction system named PML. The basic idea is to start from an ML-like programming language and add specification and proof facilities.

On the programming language side, the language unifies certain concepts: PML uses only one notion of sum types (polymorphic variants) and one notion of products (extensible records). These can then be used to encode modules and objects. PML's typing algorithm is based on a new constraint consistency check (as opposed to constraint solving).

We transform the programming language into a deduction system by adding specification and proofs into modules. Surprisinly, extending such a powerful programming language into a deduction systems requires very little work. For instance, the syntax of programs can be reused for proofs.

PML is available online

Detailed Program

On the Calculemus page, there is a graphical version of the overall conference program.

Fr 16:45Jian XuMei -- a Module System for Mechanized Mathematics Systems
17:15Clemens BallarinAlgebraic structures in Axiom and Isabelle: attempt at a comparison
Sa 09:00Christophe Raffalli(invited) PML -- a new proof assistant
10:30Claudio Sacerdoti CoenDeclarative Representation of Proof Terms
11:00Ferruccio GuidiProcedural Representation of CIC Proof Terms
11:30Stephen WattWhat Happened to Languages for Symbolic Mathematical Computation?
13:30Makarius Wenzel and Amine ChaiebSML with antiquotations embedded into Isabelle/Isar
14:00James H. Davenport and John FitchComputer Algebra and the three `E's: Efficiency, Elegance and Expressiveness
15:00(participants)Closing round table

[1] by popular we mean > 1 million users.