{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T14:26:32Z","timestamp":1777645592381,"version":"3.51.4"},"reference-count":0,"publisher":"SAGE Publications","issue":"2","license":[{"start":{"date-parts":[[2022,5,2]],"date-time":"2022-05-02T00:00:00Z","timestamp":1651449600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["Fundamenta Informaticae"],"published-print":{"date-parts":[[2022,5,2]]},"abstract":"<jats:p>\u201cThere and Back Again\u201d (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 \u201cget\u201d 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.<\/jats:p>","DOI":"10.3233\/fi-222106","type":"journal-article","created":{"date-parts":[[2022,5,3]],"date-time":"2022-05-03T11:27:19Z","timestamp":1651577239000},"page":"115-183","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":3,"title":["Getting There and Back Again"],"prefix":"10.1177","volume":"185","author":[{"given":"Olivier","family":"Danvy","sequence":"first","affiliation":[{"name":"Yale-NUS College & School of Computing, National University of Singapore,"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","published-online":{"date-parts":[[2022,5,2]]},"container-title":["Fundamenta Informaticae"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/FI-222106","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/FI-222106","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T06:32:41Z","timestamp":1777444361000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.3233\/FI-222106"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,5,2]]},"references-count":0,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2022,5,2]]}},"alternative-id":["10.3233\/FI-222106"],"URL":"https:\/\/doi.org\/10.3233\/fi-222106","relation":{},"ISSN":["0169-2968","1875-8681"],"issn-type":[{"value":"0169-2968","type":"print"},{"value":"1875-8681","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,5,2]]}}}