norvell@csri.toronto.edu (Theo Norvell) (02/01/90)
John Gateley writes
>The scheme 311 compiler had a proof of correctness. It is published as ...
The full reference is
%A William Clinger
%T The Scheme 311 compiler: an exercise in denotational semantics
%J Conference Record of the ACM Symposium on LISP and Functional Programming
%C Austin, Texas
%D July 1984
%K slfp slfp84
%P 356-364
%K correctness proof, implementation, interactive compiler
The idea of proving compilers correct goes back to John McCarthy in 1962
(see his address to the IFIP congress). A variety of work has been done since.
Theo Norvell
norvell@csri.toronto.edu
--
Send compilers articles to compilers@esegue.segue.boston.ma.us
{spdcc | ima | lotus}!esegue. Meta-mail to compilers-request@esegue.
Please send responses to the author of the message, not the poster.