Email Gateway (Aug 18 2022 at 12:12): Email Gateway (Aug 18 2022 at 12:12):From: Tobias Nipkow <nipkow@in.tum.de>
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.
Last updated: May 03 2024 at 08:18 UTC