Path: utzoo!mnetor!tmsoft!torsqnt!news-server.csri.toronto.edu!bonnie.concordia.ca!uunet!mcsun!ukc!edcastle!cs.ed.ac.uk!arshad
From: arshad@cs.ed.ac.uk (Arshad Mahmood)
Newsgroups: comp.specification
Subject: Re: Numerical Analysis/ Formal proofs
Message-ID: <6434@skye.cs.ed.ac.uk>
Date: 18 Feb 91 14:30:11 GMT
References: <2147@m1.cs.man.ac.uk>
Sender: nnews@cs.ed.ac.uk
Reply-To: arshad@lfcs.ed.ac.uk (Arshad Mahmood)
Organization: Laboratory for the Foundations of Computer Science, Edinburgh U
Lines: 23

In article <2147@m1.cs.man.ac.uk> cliff@cs.man.ac.uk (Cliff B Jones) writes:
>
>I am aware that Hoare's 1969 article mentioned the problems of
>computer arithmetic (being finite etc.) and know of some work by Tom
>Hull (I was at the Las Cruces 1972(?) conference). *But* my question
>is still can anyone point me to references which link numerical
>problems and formal program development ideas?

Not quite formal program development, but the work of Shaye Koenig on
the relationship between finite differencing and program optimization
(a la program transformation) comes to mind.

The original paper by Shaye Koenig is in the ACM TOPLAS '82 (I think),
something quite relevent is also in Richard Bird's paper on the
promotion and accumulation strategies (ACM TOPLAS, 1984).

>cliff jones

Best Wishes,

A. Mahmood
Edin. Univ.
Scotland