<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta content="text/html;charset=ISO-8859-1" http-equiv="Content-Type">
</head>
<body bgcolor="#ffffff" text="#000000">
<div class="moz-text-html" lang="x-western">
<h1>
<center>Programming Languages for Mechanized Mathematics Workshop</center>
</h1>
<center>As part of <a
href="http://www.risc.uni-linz.ac.at/about/conferences/Calculemus2007/">Calculemus
2007</a></center>
<center>Hagenberg, Austria</center>
<p>[<a class="moz-txt-link-freetext"
href="http://www.cas.mcmaster.ca/plmms07/">http://www.cas.mcmaster.ca/plmms07/</a>]</p>
<p>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 <a
href="http://www.risc.uni-linz.ac.at/about/conferences/Calculemus2007/">Calculemus
2007</a>).</p>
<p>There are various ways in which these two subjects of
<i>programming languages</i> and <i>systems for mathematics</i> meet:
</p>
<ul>
<li>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 <i>declarative</i> or <i>representational</i>
issues are avoided.</li>
<li>The <i>mathematical languages</i> 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.</li>
<li>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 <a
href="http://www.haskell.org/docon/">docon</a> being typical). There
are some promising languages on the horizon (<a
href="http://www.e-pig.org/">Epigram</a>, <a
href="http://web.cecs.pdx.edu/%7Esheard/Omega/index.html">Omega</a>)
as well as some hybrid systems (<a href="http://agda.sourceforge.net/">Agda</a>,
<a href="http://focal.inria.fr/site/index.php">Focal</a>), although
it is unclear if they are truly capable of expressing the full range of
ideas present in mathematics.</li>
<li> 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.</li>
</ul>
We are interested in all these issues. We hope that a certain synergy
will develop between those issues by having them explored in parallel.
<p>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.</p>
<p>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? </p>
<p>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 <u>EasyChair</u>. 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).</p>
<h2>Important Dates</h2>
April 25, 2007: Submission Deadline<br>
June 29-30, 2007: Workshop
<h2>Program Committee</h2>
<a href="http://www.cs.chalmers.se/%7Eaugustss">Lennart Augustsson</a>
[Credit Suisse]<br>
<a href="http://www.math.ru.nl/%7Ebosma/">Wieb Bosma</a>[Radboud
University Nijmegen, Netherlands]<br>
<a href="http://www.cas.mcmaster.ca/%7Ecarette">Jacques Carette</a>
(co-Chair) [McMaster University, Canada]<br>
<a href="http://cedric.cnam.fr/%7Edelahaye/">David Delahaye</a> [CNAM,
France]<br>
<a href="http://www.lri.fr/%7Efilliatr/">Jean-Christophe Filliâtre</a>
[CNRS and Université de Paris-Sud, France]<br>
<a href="http://www.cl.cam.ac.uk/%7Ejrh13/">John Harrison</a> [Intel
Corporation, USA]<br>
<a href="http://www4.in.tum.de/%7Ewenzelm/">Markus (Makarius) Wenzel</a>
[Technische Universität München, Germany]<br>
<a href="http://www.cs.ru.nl/%7Efreek/">Freek Wiedijk</a> (co-Chair)
[Radboud University Nijmegen, Netherlands]<br>
<a href="http://www.risc.uni-linz.ac.at/people/wwindste/">Wolfgang
Windsteiger</a> [University of Linz, Austria]<br>
<h2>Location and Registration</h2>
Location and registration information can be found on the <a
href="http://www.risc.uni-linz.ac.at/about/conferences/Calculemus2007/">Calculemus</a>
web site.
</div>
</body>
</html>