|Proving Compilers correct email@example.com (Theo Norvell) (1990-01-31)|
|Date:||Wed, 31 Jan 90 00:31:37 EST|
|From:||Theo Norvell <firstname.lastname@example.org>|
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
%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.
Return to the
Search the comp.compilers archives again.