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 113 times.
    This article's PDF has been downloaded 108 times.