On Wed, 2011-08-24 at 14:01 +0100, Tony Finch wrote:
Ezra Cooper e...@ezrakilty.net wrote:
I believe this to be a general trait of things described as
calculi--that they have some form of name-binders, but I have never
seen that observation written down.
Combinator calculi are a
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
of the properties that
polymorphic variants enjoy, so perhaps the answer lies there?
Any help gratefully received.
Regards,
Dominic Mulligan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
On Mon, 2011-02-28 at 19:37 -0700, Luke Palmer wrote:
But what I miss when using these proof assistants, and what I have my
eyes on, is a way to Search ALL The Theorems. In current proof
assistants, developments are still distributed in packages -- and a
particular development might have
