PLMMS - last call for papers

                           LAST CALL FOR PAPERS

                            Second Workshop on
             Programming Languages for Mechanized Mathematics
                              (PLMMS 2008)

          http://events.cs.bham.ac.uk/cicm08/workshops/plmms/

                        As part of CICM / Calculemus 2008
                     Birmingham, UK, 28-29 July 2008

This workshop 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 (cf. the objective of Calculemus).

The two subjects of PL and MMS meet in the following topics, which are
of particular interest to this workshop:

  * 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.