Proving Compilers correct

Theo Norvell <norvell@csri.toronto.edu>
Wed, 31 Jan 90 00:31:37 EST

          From comp.compilers
Related articles
Proving Compilers correct norvell@csri.toronto.edu (Theo Norvell) (1990-01-31)
| List of all articles for this month |
Date: Wed, 31 Jan 90 00:31:37 EST
From: Theo Norvell <norvell@csri.toronto.edu>

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




Post a followup to this message

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