Proving Compilers correct

Theo Norvell <>
Wed, 31 Jan 90 00:31:37 EST

          From comp.compilers

Related articles
Proving Compilers correct (Theo Norvell) (1990-01-31)
| List of all articles for this month |

Date: Wed, 31 Jan 90 00:31:37 EST
From: Theo Norvell <>

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

Post a followup to this message

Return to the comp.compilers page.
Search the comp.compilers archives again.