[Axiom-developer] FW: [Om] CFP: Prog. Lang for Mechanized Mathematics Workshop

[Bill Page]

I think this workshop might be of interest to Axiom developers...

Please note that the Axiom Workshop (Thursday, June 14 to Saturday,
June 16) fits nicely with some of the other related activities at
RISC Summer program:

http://www.risc.uni-linz.ac.at/about/conferences/summer2007

for example:

CoCoA School (June 18-22)
http://cocoa.dima.unige.it/conference/cocoa2007

in case you might want to prolong your stay in Hagenberg-Linz.

Perhaps the Axiom Workshop should be cross-listed at some of
these other websites?

Regards,
Bill Page.

-----Original Message-----
From: address@hidden [mailto:address@hidden On Behalf Of
Jacques Carette
Sent: March 12, 2007 5:10 PM
To: OCaml; Haskell Cafe; address@hidden; address@hidden;
address@hidden; address@hidden; address@hidden
Subject: [Om] CFP: Prog. Lang for Mechanized Mathematics Workshop


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

[http://www.cas.mcmaster.ca/plmms07/]

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.

http://www.risc.uni-linz.ac.at/about/conferences/Calculemus2007

ATT00547.txt
Description: Text document