*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Second CFP - JAR special issue for PLMMS*From*: Makarius <makarius at sketis.net>*Date*: Thu, 23 Oct 2008 11:53:55 +0200 (CEST)

Second 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/ 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 Universitaet Muenchen, Germany) * Freek Wiedijk (Radboud University Nijmegen, Netherlands)

- Previous by Date: Re: [isabelle] Problem with mutual induction
- Next by Date: Re: [isabelle] proving finite universe
- Previous by Thread: Re: [isabelle] Problem with mutual induction
- Next by Thread: [isabelle] export .thy files as xml
- Cl-isabelle-users October 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list