[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS] PLMMS 2009: Extended deadline

          The ACM SIGSAM 2009 International
        Workshop on Programming Languages for
            Mechanized Mathematics Systems
                  PLMMS 2009

           Munich, Germany; August 21, 2009

               CALL FOR PAPERS

The ACM SIGSAM 2009 International Workshop on Programming Languages
for Mechanized Mathematics Systems will be co-located with TPHOLs 2009.
Important Dates

 * Abstract submission : May 15, 2009 (Apia, Samoa time)
 * Submission deadline: May 22, 2009 (Apia, Samoa time)
 * Author notification:  June 22, 2009  * Camera ready papers: July 10, 
 * Workshop: August 21, 2009

General Information

The scope of this workshop is at 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. Areas of interest include all aspects of PL and MMS that
meet in the following topics, but not limited to:

 * 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.
 * 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 world view?

 * 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 intentionality vs
 * 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 issues have a very colorful history. Many PL innovations first
appeared in either CA or proof systems first, before migrating into
more mainstream programming languages.  This workshop is an
opportunity  to present the latest innovations in MMS design that may be 
relevant to future programming languages, or conversely novel PL 
principles that improve upon implementation and deployment of MMS.  Why 
are all the languages of mainstream CA systems untyped?  Why are the 
(strongly typed) proof assistants so much harder to use than a typical 
CAS?  What forms of polymorphism exist in mathematics?  What forms of 
dependent types may be used in mathematical modeling?  How can MMS 
regain the upper hand on issues of "genericity" and
"modularity"?  What are the biggest barriers to using a more
mainstream language as a host language for a CAS or PA/ATP?
PLMMS 2007 was held as a satellite event of, and PLMMS 2008 was
a CICM 2008 workshop.

Submission Details

  Submitted papers should be in portable document format (PDF),
  formatted using the ACM SIGPLAN style guidelines
  (http://www.acm.org/sigs/sigplan/authorInformation.htm). The length
  is restricted to 10 pages, and the font size 9pt. Each submission
  must adhere to SIGPLAN's republication policy, as explained on the
  web. Violation risks summary rejection of the offending submission.

 Papers are exclusively submitted via EasyChair

  We expect that at least one author of each accepted paper attends
  PLMMS 2009 and presents her or his paper.

  Accepted papers will appear in the ACM Digital Library.


 * http://plmms09.cse.tamu.edu/, the PLMMS 2009 workshop web site
 * http://tphols.in.tum.de/, the THOPLs 2009 conference web site

Program Committee

 * Clemens Ballarin, aicas GmbH
 * Gabriel Dos Reis, Texas A&M University (Co-Chair)
 * Jean-Christophe Filliâtre, CNRS Université Paris Sud
 * Predrag Janicic, University of Belgrade
 * Jaakko Järvi, Texas A&M University
 * Florina Piroi, Johannes Kepler University
 * Laurent Théry, INRIA Sophia Antipolis (Co-Chair)
 * Makarius Wenzel, Technische Universität München