[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: A bit further toward the flamewar

From: Ludovic Courtès
Subject: Re: A bit further toward the flamewar
Date: Fri, 14 Oct 2011 11:28:34 +0200
User-agent: Gnus/5.110018 (No Gnus v0.18) Emacs/24.0.90 (gnu/linux)

Hans Aberg <address@hidden> skribis:

> On 13 Oct 2011, at 23:14, Ludovic Courtès wrote:
>> Did you know that Coq would only compile a function when it can prove
>> that it terminates?  That’s another kind of compiler-supported proof one
>> quickly gets used to.
> Termination is a non-deducable property. They look at a intuitionistic subset 
> of programs.

Sorry, I’m not sure what you mean.

What I had in mind is what they call “well-founded recursion” [0] and
the idea that a recursive function must have a “decreasing argument” [1].



reply via email to

[Prev in Thread] Current Thread [Next in Thread]