[CakeML-dev] regexp matcher termination

Ramana Kumar Ramana.Kumar at cl.cam.ac.uk
Thu Mar 9 07:12:27 UTC 2017

Hi all,

Just checking: is there any chance we might get the termination proof
for the regular expression matcher done within a week or two? I heard
it's a very hard problem that people have already sunk a lot of time
into, so my guess is no. However, this means our top-level spec for
grep will have an annoying clunky assumption.

I guess another way to ask the question: Should I invest time in the
termination proof or in making the termination assumption prettier?


More information about the Developers mailing list