Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!tut.cis.ohio-state.edu!snorkelwacker!spdcc!esegue!compilers-sender
From: norvell@csri.toronto.edu (Theo Norvell)
Newsgroups: comp.compilers
Subject: Proving Compilers correct
Message-ID: <1990Feb1.014349.26106@esegue.segue.boston.ma.us>
Date: 1 Feb 90 01:43:49 GMT
Sender: compilers-sender@esegue.segue.boston.ma.us
Reply-To: Theo Norvell <norvell@csri.toronto.edu>
Organization: Compilers Central
Lines: 22
Approved: compilers@esegue.segue.boston.ma.us

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.