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
