Re: Compiler Correctness

Matthias Blume <find@my.address.elsewhere>
7 Feb 2006 15:36:57 -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)
[13 later articles]
| List of all articles for this month |
From: Matthias Blume <find@my.address.elsewhere>
Newsgroups: comp.compilers
Date: 7 Feb 2006 15:36:57 -0500
Organization: Compilers Central
References: 06-02-053
Keywords: theory, debug
Posted-Date: 07 Feb 2006 15:36:57 EST



"pramod" <Pramod.Patangay@gmail.com> writes:
> 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?
> [I think it's been done on some toy compilers, but realistic compilers
> are so large that the proof would be too long to be credible. -John]


Xavier Leroy: "Formal certification of a compiler back-end, or:
programming a compiler with a proof assistant." Proceedings of POPL
2006.


Post a followup to this message

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