From: [EMAIL PROTECTED] (S.D.Mechveliani)
Subject: do not write compiler in C
Date: Fri, 14 Jan 2000 09:52:17 +0300 (MSK)
> One could reply:
> "We cannot think now of such a clever compiler. It is not real."
>
> First, I think, this example with the sorting will become real soon.
Matthias Mann <[EMAIL PROTECTED]> implemented an
analysis for proving equivalence (APE) as part of his masters
thesis. It is able to prove observational equivalence of programs in a
non-strict functional core language. While I do not recall from the
top of my head and don't have his thesis in reach, if the equivalence
of insertion sort and merge sort was one of his examples, his analysis
did automatically prove some interesting equivalences.
Marko
