coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] guarded recursion and termination

From: Gert Smolka <smolka AT ps.uni-saarland.de>
To: Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] guarded recursion and termination
Date: Sun, 19 Sep 2010 19:40:12 +0200

Am 19.09.2010 14:23, schrieb Thorsten Altenkirch:

Actually Andreas Abel and myself proved termination (even though only for simple
types). See our JFP 02 paper "A Predicative Analysis of Structural
Recursion" (http://www.cs.nott.ac.uk/~txa/publ/jfp02.pdf).

This is what I was looking for. Thanks, -- Gert

[Coq-Club] guarded recursion and termination, Gert Smolka
- Re: [Coq-Club] guarded recursion and termination, Pierre Casteran
  - Re: [Coq-Club] guarded recursion and termination, Gert Smolka
    - Re: [Coq-Club] guarded recursion and termination, Thorsten Altenkirch
      - Re: [Coq-Club] guarded recursion and termination, Vladimir Voevodsky
        
        Re: [Coq-Club] guarded recursion and termination, Thorsten Altenkirch
      - Re: [Coq-Club] guarded recursion and termination, Gert Smolka
    - Re: [Coq-Club] guarded recursion and termination, Pierre Casteran
- Re: [Coq-Club] guarded recursion and termination, Thorsten Altenkirch
- Re: [Coq-Club] guarded recursion and termination, Pierre Casteran