Martin,
>The book is based around Isabelle/HOL so if you don't want to use
>Isabelle the book may not be of interest to you? I have only just
>started reading the book so I don't have any great insights to give.
Actually, Lamport's "How to write 21st Century Proofs" and
"Specifying Systems" is
On 08/05/15 10:02, d...@axiom-developer.org wrote:
Axiom Volume 13 is the start of the pile. If you find any papers
or articles that might be of interest to the goal, please let me know.
Tim,
I am currently reading Nipkow/Klien [1] just to get a top level view of
the subject (I have not looke
> Unfortunately, algorithms not only must be proved
> mathematically correct, but also be implemented correctly.
>
> There is no fail-safe way to do mathematics other than
> never leaving any "trivial" or "obvious" claims unchecked,
> by multiple referees who would have to do the hard work.
> N
