The Coq mailing list

[Frederic Blanqui <Frederic.Blanqui AT lri.fr>]

On Mon, 3 Jul 2000, Maria Joao Frade wrote:

> However, we would like to know whether someone has
> investigated modifications to the current verifications
> made in Coq so as to avoid non-terminating functions?
> We are interested  to hear about modifications on the
> guard condition rather than on type systems a la Gimenez
> ICALP'98 (actually, we came across this problem when
> trying to prove that all inductive definitions accepted by Coq
> are also accepted by a type system stemming from Gimenez
> ICALP'98 article and we would like to know what is the most
> powerful type system based on the guard predicate that is
> strongly normalizing).

Perhaps, the following papers can help you:

- Inductive Data Type Systems
or The Calculus of Algebraic Constructions
http://www.lri.fr/~blanqui/publis/

- Termination of rewriting in the Calculus of Constructions
http://www.lri.fr/~daria/papers/

Frederic Blanqui.

------------------------------------------------------------------------------
Laboratoire de Recherche en Informatique (LRI) - Equipe DEMONS
batiment 490, bureau 153, Universite Paris-Sud 91405 ORSAY (FRANCE)
tel:01 69 15 42 35 - fax:01 69 15 65 86 - web:http://www.lri.fr/~blanqui