Specifying and Verifying a Transformation of Recursive Functions into Tail-Recursive Functions

In order to build this paper we suggest using the supplied Nix Flake to do so, which already describes all the dependencies.

If using direnv:

direnv allow

In a development environment, build the document with:

tectonic specifying-verifying-tail-recursive.tex

Through Nix, this document should build flawlessly in both Linux and macOS.