[Agda] termination proofs

Nils Anders Danielsson nad at chalmers.se
Mon Sep 24 16:20:58 CEST 2012

On 2012-09-24 13:36, Serge D. Mechveliani wrote:
> Where it is specified in the Language which functions are considered
> as provably terminating?

A conservative approximation of the criterion used in Agda is described
in Section 2.5 of "Subtyping, Declaratively"

> Now: how to make a  termination	proof  as explicit as possible?

You can represent termination proofs explicitly in many different ways.
I believe that the paper "Partiality and Recursion in Interactive
Theorem Provers — An Overview" by Bove, Krauss and Sozeau
lists some of them.


More information about the Agda mailing list