[mizar] [Hol-info] New article type PROOF PEARLS in Journal of Automated Reasoning (fwd)

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

---------- Forwarded message ----------
Date: Thu, 17 Jul 2008 18:26:00 +0200
From: Tobias Nipkow <nipkow@in.tum.de>
To: hol-info@lists.sourceforge.net
Subject: [Hol-info] New article type PROOF PEARLS in Journal of Automated
    Reasoning

Journal of Automated Reasoning is very happy to announce the new article
type of

		*Proof Pearls*.

The goal of *Proof Pearls* is to disseminate insights gleaned from the
growing body of machine-checked formalizations and proofs, obtained
using both interactive and automated methods. Application areas include
the full range from pure mathematics and logic to software and hardware
verification. Proof pearls should be short communications that focus on
a few central ideas rather than extended research reports. Contributions
may include:

o a short, elegant proof of a self-standing result

o a novel way of defining a fundamental concept

o a notable approach to proving a key lemma in a larger development

o a snippet of verified code, carefully engineered to balance efficiency
with ease of verification

o a clever or impressive application of automated tools in a particular
domain

*Proof Pearls* adapt Jon Bentley's notion of a "programming pearl" to
the verification paradigm. Proof pearls should thus encapsulate
fundamental insights that are adaptable and reusable, while being
elegant and satisfying in their own right. Typical examples could be a
verification of Huffman's algorithm, a perspicuous proof of the
fundamental theorem of algebra, or a novel axiomatization of a
particular algebraic system that was discovered using automated methods.

Submissions will undergo the usual refereeing process, and will be
evaluated according to expository and theoretical merit. Systems and
formalizations should be made available online.

We look forward to your submissions
Tobias Nipkow
Editor-in-Chief
JAR

-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info