Proof Pearls
A typical TPHOLs paper represents a substantial amount of research.
However, we think there is also a place for polished exposition of
somewhat smaller efforts, provided they are interesting to the program
committee. Therefore, as an experiment, we will accept a small number
of proof pearl papers at TPHOLs2004. A proof pearl is a
concise and elegant presentation of an interesting formalization. It
should have wide appeal. Here are a few "pearl-like" examples:
An example of a non-pearl would be an exposition of how a person
proved that the square root of 2 is not rational in their favourite
theorem prover. Such an example is too simple. (By this we mean no
criticism of Wiedijk's
fascinating survey of how various proof systems supported the task
of formalizing and proving this theorem.)
A pearl will typically be shorter than a full-length research paper:
from 6 to 12 pages should suffice. A pearl should have "Proof Pearl" as
a prefix in the title of the paper; for example: Proof Pearl: An
Inconsistency in Peano Arithmetic.
Please contact the Program Chair if you have questions about the
suitability of a planned pearl.