"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.

翻译：“ There and Back Again” (TABA) 是一种编程模式, 循环电话绕过一个数据结构, 而随后的返回则绕过另一个数据结构。 文章提供了新的 TABA 示例, 改进了现有实例, 并使用 Coq 校对助理将它们的控制流程和数据流正式化。 每一个正规化都将笔和纸的证明机械化, 从而更容易“ 获取” TABA 。 此外, 文章识别并展示了 TABA 、 There and Forth 的尾尾尾补变体, 它不会回来, 而是用更多的尾查。