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
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
