How to transform an Abstract Syntax Tree (AST) to an Abstract Binding Tree (ABT)? (for machine learning fo theorem proving)
Your referenced paper doesn't define the term &quot;abstract binding trees&quot;; where did you get that phrase? (I did not look at your other references; this paper was interesting enough by itself).
The paper does define a variety of transformations on ASTs by examples, but IMHO those examples are sufficient to define or least lookup the necessary algorithms.
What I interpret the paper as saying is,  &quot;(for our GNN-based theorem prover), you can use pure ASTs, or you can use a variety of variants which perform better because they take context into account&quot;.
If you work on compiling code, you already know the value of (semantic) context over a pure context-free parsing in validating program source text (and logical formulas are just a kind of programming text).   I make this point brutally obvious here: Life After Parsing
They seem to define context in three different ways:

bidirectional links between parent and child nodes.   Having links going both directions allows context to be computed bottom up, and to have context flow from some children of a node, to be passed as context to other children.  This sounds like the value one obtains by having an attribute grammar, which has synthesized properties and inherited properties.   I didn't read the paper carefully enough to understand what information was being propagated up, or what was being propagated down, or even how their GNN accomplished this effect.   Implementing this is rather trivial: one needs child links and parent links in the nodes.

joining nodes in the AST that represent the same variable.  What this is doing is taking into account scoping rules in the language, and amounts to replacing variable names by symbol table references.  They argue that the type information associated with the symbols should be included, which you get for  &quot;free&quot; if your symbol table includes type information, which any serious symbol table does.  Implementing this requires that your AST processing machinery be augmented with symbol tables, and that the AST is processed to replace identifier nodes with symbol table entries (well, with the content of the appropriate symbol table entry).   This is hard to do if your langauge is complex (e.g, symbol tables for C++ will make your head explode) you need an extremely organized attack to build/use these; this is part of the reason that building compiler front ends is hard.  But for the HOL representations being used by the authors, the &quot;symbol&quot; tables are pretty simple and you can probably do this in an ad hoc way with a tree-scanning procedure.

Merging common subtrees honoring variable type information into single trees.  This is classically what common sub-expression elimination does.   Its apparent value in this paper is that it can dramatically shrink the size of the tree and therefore the implied amount of work it takes to process the tree. (You can get an overly compressed tree for free if you use a GLR parser which produces maximally shared subforests which happen to also include expression trees, but  you have to split out shared subtrees based on type information after the fact).  I note this looks to me not so much as context usage but &quot;merely&quot; size reduction.


TLDR:  The authors appear to implementing classic compiler front end building techniques and algorithms to convert ASTs into what amounts to Directed Acyclic Graphs that encode type information for different variables.
[FWIW, a generalized AST-processing engine I build called DMS has: a) bidirectional links between parent and child nodes, b) shared subtrees via GLR parsing c) symbol table definition methods, d) attribute-grammar definition/execution which is easily used to scan  ASTs to link leaves to symbol table entries. AFAICT, DMS sort of does everything this paper suggests doing.  This is because you pretty much always need at least the results of all this to process any kind of AST in a semantically sensible way].
HTH.