Inductive type theories, as used in systems like Coq or Lego [11,14,4], provide a systematic approach to program recursive functions over inductive data-structures and to reason about these functions.
Recursive computation is described by reduction rules, included in the type system under the name ι-reduction. If t is an element of a recursive type, f is a recursive function over that type and v is the value of f(t), then the equality f(t) = v is a simple tautology, because f(t) and v are equal modulo ι-reduction.