Re: [Axiom-mail] address@hidden: Re: Axiom Journal]

[Mike Dewar]

On Fri, Nov 29, 2002 at 04:20:00PM -0500, Tim Daly wrote:
<snip>
> I'm also in discussions about actually proving the algorithms
> with some formal logic which would make the publications unique.
> If I can build support in the program proof community for proving
> submitted algorithms as part of the "review" process then the 
> Journal would offer something unique and useful as an incentive.

If you're interested in proving the correctness of Axiom's algorithms
you should check out the work by Tom Kelsey and Martin Dunstan, both
former PhD students of Ursula Martin's at St Andrews.   They generated
Larch specifications of all the types in the Axiom library and actually
found some bugs as a result!  Tom still works at St Andrews and his home
page at http://kininvie.dcs.st-and.ac.uk/~tom/ includes his thesis.
Martin is now working on the Scottish space programme in Dundee
(really!) but still has a home page at St Andrews,
http://www-theory.dcs.st-and.ac.uk/~mnd/, which includes his thesis
(follow the "academic publications" link).

Mike.

_____________________________________________________________________
This message has been checked for all known viruses by Star Internet
delivered through the MessageLabs Virus Scanning Service. For further
information visit http://www.star.net.uk/stats.asp or alternatively call
Star Internet for details on the Virus Scanning Service.