[Axiom-developer] Programming Languages and Mechanised Mathematics -- deadline extension

[Jacques Carette]

[Extended deadline: submissions now due May 2nd, 2007]

Programming Languages for Mechanized Mathematics Workshop

As part of Calculemus 2007
<http://www.risc.uni-linz.ac.at/about/conferences/Calculemus2007/>
Hagenbergs, Austria
June 29-30, 2007.

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
<http://www.risc.uni-linz.ac.at/about/conferences/Calculemus2007/>).

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 <http://www.haskell.org/docon/> being typical). There are
    some promising languages on the horizon (Epigram
    <http://www.e-pig.org/>, Omega
    <http://web.cecs.pdx.edu/%7Esheard/Omega/index.html>) as well as
    some hybrid systems (Agda <http://agda.sourceforge.net/>, Focal
    <http://focal.inria.fr/site/index.php>), 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''[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, 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

May 02, 2007: Submission Deadline (Extended!)
May 30, 2007: 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 and registration information can be found on the Calculemus
<http://www.risc.uni-linz.ac.at/about/conferences/Calculemus2007/> web site.

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