FW: [Om] Programming Languages and Mechanised Mathematics -- deadlineextension

 In case any readers of this list are interested in the subject line..
RJF

> -----Original Message-----
> From: om-bounces at openmath.org 
> [mailto:om-bounces at openmath.org] On Behalf Of Jacques Carette
> Sent: Wednesday, April 25, 2007 7:02 AM
> To: axiom-developer at nongnu.org; 'aldor-l'; Haskell Cafe; 
> OCaml; epigram at durham.ac.uk; felix-language; 
> metaocaml-hackers-l at cs.rice.edu; om at openmath.org
> Subject: [Om] Programming Languages and Mechanised 
> Mathematics -- deadlineextension
> 
> [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/Calculemus20
07/> web site.
> 
> --------------------------------------------------------------
> ---------------
> [1] by popular we mean > 1 million users.
> 
> _______________________________________________
> Om mailing list
> Om at openmath.org
> http://openmath.org/mailman/listinfo/om
>