Отправляет email-рассылки с помощью сервиса Sendsay

Система компьютерной алгебры GAP

Подписаться Бесплатная «Серебряная» новостная рассылка . Временно не выходит ,возобновит выход - нет информации Подписчиков 783 RSS
←   Март 2008   →
 1
 2
 3
 4
 5
05.03.2008
08:06:10
18:42:16
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31


За последние 60 дней ни разу не выходила


Сайт рассылки: http://www.gap-system.org/ukrgap/
Открыта: 05-02-2002

Автор
Александр Борисович Коновалов

Статистика

783 подписчиков
0 за неделю
←   Все выпуски   →

Система компьютерной алгебры GAP - 2nd CFP: PLMMS 2008, Birmingham, UK, 28-29 July 2008


  SECOND CALL FOR PAPERS

* UPDATE: Post-workshop proceedings in Journal of Automated Reasoning
* UPDATE: Invited talk by Conor McBride

                          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.

* 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 intentionality 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 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. Some examples include type
inference, dependent types, generics, term-rewriting, first-class
types, first-class expressions, first-class modules, code extraction
etc. However, such innovations were never aggressively pursued by
builders of MMS, but often reconstructed by programming language
researchers. 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.

We also want to critically examine what has worked, and what has not.
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?


Invited Talk
------------

Conor McBride (Alta Systems, Northern Ireland) will give an invited
talk.


Submission
----------

Submission works through EasyChair
http://www.easychair.org/conferences/?conf=plmms2008

Two kinds of papers will be considered:

* Full research papers may be up to 12 pages long. Authors of
 accepted papers are expected to present their work on the workshop
 in a regular talk.

* Position papers may be up to 4 pages long. The workshop
 presentation of accepted position papers consists of two parts: a
 stimulating statement of certain issues or challenges by the
 author, followed by a discussion in the plenum.

Papers should use the usual ENTCS style http://www.entcs.org/prelim.html
(11 point version), and will be reviewed by the program
committee. Informal workshop proceedings will be circulated as a
technical report.

Moreover there will be post-workshop proceedings of improved research
papers, or position papers that have been completed into full papers,
to appear in a special issue of the Journal of Automated Reasoning.
There will be a separate submission and review phase for this, where
papers from both PLMMS 2007 and 2008 will be considered.


Programme Committee
-------------------

 Jacques Carette (Co-Chair) (McMaster University, Canada)
 John Harrison              (Intel Corporation, USA)
 Hugo Herbelin              (INRIA, Ecole polytechnique, France)
 James McKinna              (Radboud University Nijmegen, Netherlands)
 Ulf Norell                 (Chalmers University, Sweden)
 Bill Page
 Christophe Raffalli        (Universite de Savoie, France)
 Josef Urban                (Charles University, Czech Republic)
 Stephen Watt               (ORCCA, University of Western Ontario, Canada)
 Makarius Wenzel (Co-Chair) (Technische Universitaet Muenchen, Germany)
 Freek Wiedijk              (Radboud University Nijmegen, Netherlands)


Important Dates
---------------

* Submission deadline - 5 May 2008
* Notification of acceptance - 6 June 2008
* Final version - 7 July 2008 (approximately)
* Workshop - 28-29 July 2008
В избранное