[TYPES/announce] Programming Languages for Mechanized Mathematics Workshop

[Jacques Carette]

[The main aspect which separates many approaches to mechanized 
mathematics is the importance (or lack thereof) of types.  Most of 
mathematics requires dependent types at some level or another, making 
this an interesting testing ground for types members]


  Programming Languages for Mechanized Mathematics Workshop

As part of Calculemus 2007 
<http://www.risc.uni-linz.ac.at/about/conferences/Calculemus2007/>

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 
<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'' 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 <http://www.cs.chalmers.se/%7Eaugustss> [Credit Suisse]
Wieb Bosma <http://www.math.ru.nl/%7Ebosma/>[Radboud University 
Nijmegen, Netherlands]
Jacques Carette <http://www.cas.mcmaster.ca/%7Ecarette> (co-Chair) 
[McMaster University, Canada]
David Delahaye <http://cedric.cnam.fr/%7Edelahaye/> [CNAM, France]
Jean-Christophe Filliâtre <http://www.lri.fr/%7Efilliatr/> [CNRS and 
Université de Paris-Sud, France]
John Harrison <http://www.cl.cam.ac.uk/%7Ejrh13/> [Intel Corporation, USA]
Markus (Makarius) Wenzel <http://www4.in.tum.de/%7Ewenzelm/> [Technische 
Universität München, Germany]
Freek Wiedijk <http://www.cs.ru.nl/%7Efreek/> (co-Chair) [Radboud 
University Nijmegen, Netherlands]
Wolfgang Windsteiger <http://www.risc.uni-linz.ac.at/people/wwindste/> 
[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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20070312/0888ff79/attachment.htm