Lambda the Ultimate

Cyclic Proofs for First-Order Logic with Inductive Definitions, James Brotherston, in Proceedings of TABLEAUX 2005

We consider a cyclic approach to inductive reasoning in the setting
of first-order logic with inductive definitions. We present a proof
system for this language in which proofs are represented as finite,
locally sound derivation trees with a "repeat function"
identifying cyclic proof sections. Soundness is guaranteed by a
well-foundedness condition formulated globally in terms of
\emph{traces} over the proof tree, following an idea due to Sprenger
and Dam. However, in contrast to their work, our proof system does
not require an extension of logical syntax by ordinal variables.

This technique of making potentially cyclic proof-graphs is really nice since it makes the connection between recursive definitions in a functional programming language and a proof structure very obvious. There is no need to specify the inductive principle ahead of time, you can simply structure the proof tree as you would your functional code.