[mizar] Special issue on Programming Languages and Mechanized Mathematics Systems (JAR) (fwd)

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

---------- Forwarded message ----------
Date: Tue, 9 Sep 2008 20:52:11 +0200 (CEST)
From: Makarius <makarius@sketis.net>
To: isabelle-users@cl.cam.ac.uk
Subject: [isabelle] Special issue on Programming Languages and Mechanized
    Mathematics Systems (JAR)

				CALL FOR PAPERS

Special issue on Programming Languages and Mechanized Mathematics Systems

	      	 	Journal of Automated Reasoning

[See HTML version at http://www.cas.mcmaster.ca/~carette/jplmms/cfp.html ]

Context

   This special issue is focused on the intersection of programming
   languages (PL) and mechanized mathematics systems (MMS). The latter
   category subsumes present-day computer algebra systems (CAS),
   interactive proof assistants (PA), and automated theorem provers (ATP),
   all heading towards fully integrated mechanized mathematical assistants
   that are expected to emerge eventually.

   The two subjects of PL and MMS meet in many interesting ways, in
   particular in the following main topics of this journal issue.

     * Dedicated input languages for MMS: covers all aspects of languages
       intended for the user to deploy or extend the system, both
       algorithmic and declarative ones. Typical examples are tactic
       definition languages such as Ltac in Coq, mathematical proof
       languages as in Mizar or Isar, or specialized programming languages
       built into CA systems. Of particular interest are the semantics of
       those languages, especially when current ones are untyped.
     * Mathematical modeling languages used for programming: covers the
       relation of logical descriptions vs. algorithmic content. For
       instance the logic of ACL2 extends a version of Lisp, that of Coq
       is close to Haskell, and some portions of HOL are similar to ML and
       Haskell, while Maple tries to do both simultaneously. Such
       mathematical languages offer rich specification capabilities, which
       are rarely available in regular programming languages. How can
       programming benefit from mathematical concepts, without limiting
       mathematics to the computational worldview?
     * Programming languages with mathematical specifications: covers
       advanced "mathematical" concepts in programming languages that
       improve the expressive power of functional specifications, type
       systems, module systems etc. Programming languages with dependent
       types are of particular interest here, as is intensionality vs
       extensionality.
     * Language elements for program verification: covers specific means
       built into a language to facilitate correctness proofs using MMS.
       For example, logical annotations within programs may be turned into
       verification conditions to be solved in a proof assistant
       eventually. How need MMS and PL to be improved to make this work
       conveniently and in a mathematically appealing way?

   These topics have been addressed in the PLMMS 2007
   http://www.cas.mcmaster.ca/plmms07/ and PLMMS 2008
   http://events.cs.bham.ac.uk/cicm08/workshops/plmms/ workshops
   (associated with Calculemus http://www.calculemus.net/). While the
   journal issue emerges from that community, submission is open to
   everyone interested in any of these topics!

Submission

   Manuscripts should not have been previously published in archival
   journals nor have been submitted to, or be in consideration for, any
   journal or conference. Significantly revised and enhanced papers
   published in workshop or conference proceedings are welcome. All
   submissions will be reviewed according to scholarly standards for
   scientific journal publications. See also the general JAR submission
   policies.

   We suggest a page limit of approximately 25 pages, using the LaTeX
   macros ftp://ftp.springer.de/pub/tex/latex/svjour3/global.zip
   provided by Springer. Instead of using the Springer online
   submission system, please submit papers in PDF through EasyChair
   http://www.easychair.org/conferences/?conf=jplmms2008

Important dates

     * Submission deadline: 10th November 2008.
     * Notification: January 16th 2009.
     * Final versions: March 30th 2009.

Editors of the special issue

     * Jacques Carette (McMaster University, Canada)
     * Makarius Wenzel (Technische Universitt Mnchen, Germany)
     * Freek Wiedijk   (Radboud University Nijmegen, Netherlands)