The Coq mailing list

[Frederic Blanqui <blanqui AT loria.fr>]

On Wed, 27 Sep 2006, Stefan Monnier wrote:

> Could someone point me to a paper presenting formally the constraints placed 
> on the use of "match" and "Fixpoint" to guarantee termination (in Coq or in 
> some simplified variant)?  Ideally, this paper would come with a proof of 
> strong normalization (maybe via reducibility to the usual Elim form).

the constraints are the same as with the elim construction: recursive calls 
must be done on arguments structurally smaller. for a study of coq with 
fixpoints, you should look at philippe audebaud's papers. note that there are 
more powerful termination criteria allowing non structurally smaller 
arguments.