Algorithms, term rewriting and compile time reflection

[Andrei Alexandrescu via Digitalmars-d]

On 10/27/14 6:53 PM, deadalnix wrote:
> On Tuesday, 28 October 2014 at 01:10:18 UTC, Andrei Alexandrescu
> wrote:
>> On 10/23/14 2:41 AM, thedeemon wrote:
>>> To scare you well, here, for example, is my Smoothsort implementation in
>>> ATS
>>> http://stuff.thedeemon.com/lj/smooth_dats.html
>>> that includes proofs that the array really gets sorted and the Leonardo
>>> heaps used in the process have proper form and properties. Writing it
>>> took me a few weeks. You don't want to turn D into this mess. ;)
>>
>> I recall there was an earlier implementation of a statically-checked
>> sort, maybe in Agda? It wouldn't typecheck if the output array weren't
>> sorted.
>>
>> Andrei
>
> Sound like madness :) I'd love to see it.

Looked again for it, couldn't find it. Got this other one instead:

http://lara.epfl.ch/~psuter/articles/BlancETAL13OverviewLeonVerificationSystem.pdf


Andrei