Re: [isabelle] mergesort



On 10/28/2012 12:53 AM, Makarius wrote:
On Wed, 24 Oct 2012, Christian Sternagel wrote:

On 10/23/2012 08:17 PM, Makarius wrote:
(Next time I will tell a story how an efficient and fully verified
merge-sort function included in the core sources caused several days of
worries.)

Please tell the story.

I will try, but it has to be shorter than usual: I've just returned from
travel and I am preparing for the next departure starting in 1.5 days.


I'm particularly interested since in the near future I was going to
suggest to run some tests whether it would make sense
(performance-wise) to replace the existing sorting algorithm in the
Isabelle sources by the one from (sorry for the self-advertisement):

 http://link.springer.com/article/10.1007/s10817-012-9260-7

The website seems to be down at the moment, and it does not look like a
publicly available thing anyway (without paying extra).
Well, I paid a lot extra to make it "open access" so it better be publicly available. From my location this works, please let me know if it is not the case from elsewhere.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.