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 "fr
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
2011/6/21 Jason Dagit
> On Tue, Jun 21, 2011 at 3:31 AM, Uli Kastlunger
> 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 Compi
On Tue, Jun 21, 2011 at 3:31 AM, Uli Kastlunger 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 out of a specif
On Tue, Jun 21, 2011 at 3:31 AM, Uli Kastlunger 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 out of a speci
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 ea
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
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
___
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 compil
On Tue, Feb 3, 2009 at 12:28 AM, Don Stewart wrote:
> dbueno:
>> On Mon, Feb 2, 2009 at 15:04, Don Stewart 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 so
On Mon, Feb 2, 2009 at 10:04 PM, Don Stewart 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)
> t
dbueno:
> On Mon, Feb 2, 2009 at 15:04, Don Stewart 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 t
On Mon, Feb 2, 2009 at 15:04, Don Stewart 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)
> targ
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
On Sun, Feb 1, 2009 at 12:54 PM, Paulo J. Matos 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 into Haskell,
yo
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
verifyi
16 matches
Mail list logo
