Re: Reasons why you don't prove your programs are correct

gateley@m2.csc.ti.com (John Gateley)
26 Jan 90 18:45:25 GMT

          From comp.compilers
Related articles
Reasons why you don't prove your programs are correct steve@hubcap.clemson.edu (1990-01-05)
Re: Reasons why you don't prove your programs are correct keithd@anvil.oz.au (1990-01-12)
Re: Reasons why you don't prove your programs are correct mayer@iuvax.cs.indiana.edu (Mayer Goldberg) (1990-01-17)
Re: Reasons why you don't prove your programs are correct pardo@cs.washington.edu (1990-01-22)
Re: Reasons why you don't prove your programs are correct pardo@cs.washington.edu (1990-01-24)
Re: Reasons why you don't prove your programs are correct gateley@m2.csc.ti.com (1990-01-26)
| List of all articles for this month |
From: gateley@m2.csc.ti.com (John Gateley)
Newsgroups: comp.compilers
Date: 26 Jan 90 18:45:25 GMT
References: <7578@hubcap.clemson.edu> <1990Jan16.232703.2368@esegue.segue.boston.ma.us> <1990Jan22.234119.7002@esegue.segue.boston.ma.us> <1990Jan24.220734.223@esegue.segue.boston.ma.us>
Organization: TI Computer Science Center, Dallas

In article <1990Jan24.220734.223@esegue.segue.boston.ma.us> pardo@cs.washington.edu (David Keppel) writes:
>A related issue: do you prove your compiler correct?


The scheme 311 compiler had a proof of correctness. It is published
as "The Scheme 311 Compiler, An Exercise in Denotational Semantics" in
a conference proceedings (my copy doesn't have the name). The stuff
at the bottom is: (c) 1984 ACM 0-89791-142-3/84/008/0356 $00.75
and it is probably one of: the lisp and functional programing conference,
POPL, or the compiler conference.


John
gateley@m2.csc.ti.com




Post a followup to this message

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