Stack graphs is the formalism that we've put together at GitHub to power Precise Code Navigation. It's based on the scope graphs framework from Eelco Visser's group at TU Delft.
We have published one paper about stack graphs so far.
Kutsia2007 describes sequence unification, which is the unification strategy we use in the stack graph partial path stitching algorithm. §6.3, in particular, shows that sequence unification is unitary if “sequence variables occur only int he last argument positions in terms”.