Termination Checking in Agda Core

Abstract

Dependently typed languages and proof assistants such as Agda and Rocq improve the reliability of mathematical proofs and programs by representing logical propositions as types and proofs as programs inhabiting those types. Through the Curry--Howard correspondence, typechecking becomes proof checking, allowing correctness guarantees to be established by construction.

However, these guarantees ultimately rely on the correctness of the language implementation itself. Components such as typecheckers, conversion checkers, and termination checkers are typically implemented as algorithms whose correctness must be trusted independently from the theory they are intended to enforce.

Agda Core is a core language for Agda implemented in Agda itself, where language judgements are represented directly as dependent types and checking procedures become programs constructing evidence of those judgements. This thesis investigates how the same methodology can be applied to termination checking.

Termination checking is a fundamental component of dependently typed languages, since unrestricted recursion may compromise normalization and logical consistency. We explore how termination criteria can be represented as formal specifications together with executable proof-search procedures producing explicit certificates that the criteria hold.

We first study the guard condition, a structural recursion criterion based on descending recursive arguments, and implement a certified checker producing explicit evidence that the criterion holds. We then investigate the size change principle, a stronger termination criterion capable of handling a wider class of recursive and mutually recursive definitions. We formalize the corresponding rules in the same framework and discuss the challenges involved in constructing a fully executable checker for them.

More generally, this work explores the separation between declarative specifications of termination criteria and the algorithms used to search for certificates satisfying them. By expressing termination arguments directly in the type theory of the implementation language, the resulting infrastructure becomes simultaneously executable, inspectable, and partially verified.