  "There and Back Again" (TABA) is a programming pattern where the recursive
calls traverse one data structure and the subsequent returns traverse another.
This article presents new TABA examples, refines existing ones, and formalizes
both their control flow and their data flow using the Coq Proof Assistant. Each
formalization mechanizes a pen-and-paper proof, thus making it easier to "get"
TABA. In addition, this article identifies and illustrates a tail-recursive
variant of TABA, There and Forth Again (TAFA) that does not come back but goes
forth instead with more tail calls.
