## CFP: Programming Languages for Mechanized Mathematics Workshop

Programming Languages for Mechanized Mathematics Workshop As part of Calculemus 2007 Hagenberg, Austria

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).

## Comment viewing options

### How do I make a 'teaser' seperate from the body?

I did not want the full text to appear on the front page, just a few lines. I don't know how to do this :-(. My apologies for 'taking over' the front page of LtU, I did not want to do that. Please tell me how to edit this down to something friendlier!

### We don't have a mechanism to

We don't have a mechanism to do that automatically. What you should do is put the full message as a comment (reply) to the home page story (which will be the teaser).

Ok, done, thanks

### Actually...

I believe you can use the following tag:

<!--break-->


To specify where the teaser should end. I think at one point, this didn't work because we had the automatic teaser cutoff length set to "unlimited", but I think that was fixed by an upgrade, and it seems to work now.

### I think the automatic teaser

I think the automatic teaser cutoff length is still set to "unlimited". Yesterday, I got to thinking about experimenting with this feature.

### Full CFP

Programming Languages for Mechanized Mathematics Workshop

As part of Calculemus 2007
Hagenberg, Austria

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:

• Many systems for mathematics contain a dedicated programming
language. For instance, most computer algebra systems contain a
dedicated language (and are frequently built in that same language);
some proof assistants (like the Ltac language for Coq) also have
an embedded programming language. Note that in many instances
this language captures only algorithmic content, and
declarative or representational issues are
avoided.
• The mathematical languages of many systems for mathematics
are very close to a functional programming language. For
instance the language of ACL2 is just Lisp, and the language
of Coq is very close to Haskell. But even the mathematical
language of the HOL system can be used as a functional
programming language that is very close to ML and Haskell.
On the other hand, these languages also contain very rich
specification capabilities, which are rarely available in
most computation-oriented programming languages. And even
then, many specification languages ((B, Z, Maude, OBJ3, CASL, etc)
can still teach MMSes a trick or two regarding representational
power.
• Conversely, functional programming languages have been getting
"more mathematical" all the time. For instance, they seem to have
discovered the value of dependent types rather recently. But
they are still not quite ready to 'host' mathematics (the non-success
of docon being typical).
There are some promising languages on the horizon (Epigram, Omega) as
well as some hybrid systems (Agda, Focal), although it is
unclear if they are truly capable of expressing the full range of ideas
present in mathematics.
• Systems for mathematics are used to prove programs correct.
(One method is to generate "correctness conditions" from a
program that has been annotated in the style of Hoare logic
and then prove those conditions in a proof assistant.) An
interesting question is what improvements are needed for
this both on the side of the mathematical systems and on the
side of the programming languages.

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'' 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, with a more
formal version to appear later. We are
looking into having the best papers completed into full papers
and published as a special issue of a Journal (details to follow).

Important Dates
April 25, 2007: Submission Deadline
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]
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 and registration information can be found on the
Calculemus web site.

### Deadline update

Papers (and position papers) are now due May 02, 2007. They can be submitted through EasyChair.

### PLMMS 2008

There will be a 2nd installment of the Programming Languages for Mechanized Mathematics workshop. Conor McBride, whose work has been frequently discussed here will be the invited speaker. For those who do not recognize the names from the Program Committee, we have some people representing Coq, Isabelle, Hol light, Epigram, Axiom, PML, Aldor, Mizar and Maple.