Olivier Danvy - Getting There and Back Again

fi:9159 - Fundamenta Informaticae, May 6, 2022, Volume 185, Issue 2
Getting There and Back Again

Authors: Olivier Danvy

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


Volume: Volume 185, Issue 2
Published on: May 6, 2022
Accepted on: March 16, 2022
Submitted on: March 2, 2022
Keywords: Computer Science - Programming Languages


Share

Consultation statistics

This page has been seen 73 times.
This article's PDF has been downloaded 54 times.