2011/6/21 Jason Dagit dag...@gmail.com
On Tue, Jun 21, 2011 at 3:31 AM, Uli Kastlunger squar...@gmail.com
wrote:
Hello Haskell fellows,
recently there has been a huge progress in generating real programs by
specifying them in interactive theorems prover like Isabelle or Coq, in
I'm no expert with compcert, but as I understand it their approach is
to only do semantic preserving changes to the program at each step in
the translation from C source to binary. I'm not sure what they used
as their specification of C and it seems like the correctness of their
approach would
On Wed, Jun 22, 2011 at 8:11 AM, Dominic Mulligan
dominic.p.mulli...@googlemail.com wrote:
There's a second (haha) approach, which I use basically every day.
Use the typing language fragment from a strongly typed programming
language to express a specification, and then rely on free
Hello Haskell fellows,
recently there has been a huge progress in generating real programs by
specifying them in interactive theorems prover like Isabelle or Coq, in
particular a verified C Compiler has been generated out of a specification
in Coq [0]. Furthermore it is often stated, that it is
On Tue, Jun 21, 2011 at 3:31 AM, Uli Kastlunger squar...@gmail.com wrote:
Hello Haskell fellows,
recently there has been a huge progress in generating real programs by
specifying them in interactive theorems prover like Isabelle or Coq, in
particular a verified C Compiler has been generated
On Tue, Jun 21, 2011 at 3:31 AM, Uli Kastlunger squar...@gmail.com wrote:
Hello Haskell fellows,
recently there has been a huge progress in generating real programs by
specifying them in interactive theorems prover like Isabelle or Coq, in
particular a verified C Compiler has been generated
On Mon, Feb 2, 2009 at 10:04 PM, Don Stewart d...@galois.com wrote:
pocmatos:
Hi all,
Much is talked that Haskell, since it is purely functional is easier
to be verified. However, most of the research I have seen in software
verification (either through model checking or theorem proving)
On Tue, Feb 3, 2009 at 12:28 AM, Don Stewart d...@galois.com wrote:
dbueno:
On Mon, Feb 2, 2009 at 15:04, Don Stewart d...@galois.com wrote:
pocmatos:
Hi all,
Much is talked that Haskell, since it is purely functional is easier
to be verified. However, most of the research I have
Excerpts from Paulo J. Matos's message of Tue Feb 03 02:31:00 -0600 2009:
Any references to publications related to this?
While it's not Haskell, this code may be of interest to you:
http://pauillac.inria.fr/~xleroy/bibrefs/Leroy-compcert-06.html
This paper is about the development of a
Excerpts from Austin Seipp's message of Tue Feb 03 03:40:47 -0600 2009:
...
After noticing that I didn't give a link to the code in the last
message, I searched and found this more up to date page I think:
http://compcert.inria.fr/doc/index.html
Austin
State of the art is translating subsets of Haskell to Isabelle, and
verifying them. Using model checkers to verify subsets, or extracting
Haskell from Agda or Coq.
Don, can you give some pointers to literature on this, if any? That
is, any documentation of a verification effort of Haskell code
pocmatos:
Hi all,
Much is talked that Haskell, since it is purely functional is easier
to be verified. However, most of the research I have seen in software
verification (either through model checking or theorem proving)
targets C/C++ or subsets of these. What's the state of the art of
On Mon, Feb 2, 2009 at 15:04, Don Stewart d...@galois.com wrote:
pocmatos:
Hi all,
Much is talked that Haskell, since it is purely functional is easier
to be verified. However, most of the research I have seen in software
verification (either through model checking or theorem proving)
dbueno:
On Mon, Feb 2, 2009 at 15:04, Don Stewart d...@galois.com wrote:
pocmatos:
Hi all,
Much is talked that Haskell, since it is purely functional is easier
to be verified. However, most of the research I have seen in software
verification (either through model checking or
On Sun, Feb 1, 2009 at 12:54 PM, Paulo J. Matos pocma...@gmail.com wrote:
What's the state of the art of automatically
verifying properties of programs written in Haskell?
This is a large field that isn't as black and white as many people
frame it. You can write a proof [1] then translate that
Hi all,
Much is talked that Haskell, since it is purely functional is easier
to be verified.
However, most of the research I have seen in software verification
(either through model checking or theorem proving) targets C/C++ or
subsets of these. What's the state of the art of automatically
16 matches
Mail list logo
