Getting There and Back Again

TL;DR

This paper formalizes the TABA programming pattern using Coq, introduces a new variant called TAFA, and provides mechanized proofs to clarify their control and data flow.

Contribution

It presents formal Coq proofs for TABA and introduces TAFA, a tail-recursive variant that extends the pattern's applicability.

Findings

Formalization of TABA control and data flow in Coq

Introduction of TAFA, a tail-recursive variant of TABA

Mechanized proofs simplify understanding of TABA patterns

Abstract

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