<div dir="ltr">On Thu, Sep 4, 2014 at 6:06 PM, Frédéric Blanqui <span dir="ltr"><<a href="mailto:frederic.blanqui@inria.fr" target="_blank">frederic.blanqui@inria.fr</a>></span> wrote:<br><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div bgcolor="#FFFFFF" text="#000000"><div>
</div><span class=""></span>Hi.<br>
<br>
You may be interested in the works of Bellantoni, Marion, Avanzini
& Moser, ... See for instance<br>
- <a href="http://dx.doi.org/10.2168/LMCS-9(4:9)2013" target="_blank">http://dx.doi.org/10.2168/LMCS-9(4:9)2013</a><br>
- <a href="http://dx.doi.org/10.4230/LIPIcs.RTA.2011.123" target="_blank">http://dx.doi.org/10.4230/LIPIcs.RTA.2011.123</a><br>
to cite just very few papers on this topic.<span class="HOEnZb"><font color="#888888"></font></span><br></div></blockquote></div><br>Thank you for the references. Looks like those articles together propose, well, let’s say a programming language, that encodes only functions running in exponential time.<br></div><div class="gmail_extra">It seems to me that this is not particularly interesting just because there are pretty simple typesystems that guarantee that only terminating programs will typecheck and, furthermore, that all the primitive recursive functions can be typed (see e.g. “<a href="http://www2.tcs.ifi.lmu.de/~abel/publications.html#rairo04">Termination Checking with Types</a>”). Together with the widely known fact that a function is PR iff its running time is bounded by a PR function this means that this typesystem types all the exponential time functions and many others.<br>So those works are probably interesting from the term-rewriting point of view but bring nothing new into our world of checking termination by typing.<br><br>Please, correct me if I missed something!<br></div></div>