Re: Compiler Correctness

"Daniel C. Wang" <danwang74@gmail.com>
7 Feb 2006 15:37:28 -0500

          From comp.compilers
Related articles
Compiler Correctness Pramod.Patangay@gmail.com (pramod) (2006-02-07)
Re: Compiler Correctness find@my.address.elsewhere (Matthias Blume) (2006-02-07)
Re: Compiler Correctness danwang74@gmail.com (Daniel C. Wang) (2006-02-07)
Re: Compiler Correctness neelk@cs.cmu.edu (Neelakantan Krishnaswami) (2006-02-07)
Re: Compiler Correctness neelk@cs.cmu.edu (Neelakantan Krishnaswami) (2006-02-11)
Re: Compiler Correctness danwang74@gmail.com (Daniel C. Wang) (2006-02-11)
Re: Compiler Correctness torbenm@app-1.diku.dk (2006-02-11)
Re: Compiler Correctness henry@spsystems.net (2006-02-11)
Re: Compiler Correctness Sid.Touati@inria.fr (Sid Touati) (2006-02-11)
[12 later articles]
| List of all articles for this month |
From: "Daniel C. Wang" <danwang74@gmail.com>
Newsgroups: comp.compilers
Date: 7 Feb 2006 15:37:28 -0500
Organization: Compilers Central
References: 06-02-053
Keywords: theory, debug
Posted-Date: 07 Feb 2006 15:37:28 EST

See Xavier Leroy's recent work in POPL06.


http://portal.acm.org/citation.cfm?id=1111037.1111042


His is not the first, attempt.


http://csdl2.computer.org/persagen/DLAbsToc.jsp?resourcePath=/dl/proceedings/&toc=comp/proceedings/sefm/2005/2435/00/2435toc.xml&DOI=10.1109/SEFM.2005.51


Note, both proofs are machine checked. So the credibility of the
proofs is not much in doubt. Personally, while I find these results
very interesting, there are simpler ways to achieve their goals.


pramod wrote:
> I have a simple question. Can we prove that a compiler is correct? I
> mean we are given a language with it's syntax and semantics and a
> compiler whose correctness needs to be proved. Is this theoretically
> possible?

Post a followup to this message

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