PL papers tend to use lots of notation.
To manage this, paper sources usually include a "macros.tex" containing a slew of \newcommands, defining wonderful languages of terms and naming all the clever judgments and syntactic sugar.
While notation can increase clarity, it can cause difficulty to readers, who haven't had the hundreds of hours of practice the authors have had using and reading those intricate strings of symbols, and internalizing their precedences and meaning. Readers will forget what things denote and will have to scroll up and down repeatedly in a careful reading of the work.
In an attempt to alleviate this and make my work more accessible, I've been using a small set of macros to enable jump-to-definition for the important (and obscure) symbols:
% somewhere above
\usepackage[colorlinks=true]{hyperref}
% meta-commands for defining notation
\newcommand\notationlink[2]{\hyperlink{#1}{\normalcolor #2}}
\newcommand\notationtarget[2]{{\hypertarget{#1}{}}#2}
\newcommand*{\notation}[2]{%
\expandafter\newcommand\csname #1\endcsname{\notationlink{#1}{#2}}%
\expandafter\newcommand\csname #1Def\endcsname{\notationtarget{#1}{}}}
The idea is essentially to link uses of notation to their definitions. All that's really needed for that is to pepper \hyperlink and \hypertarget everywhere, and this is what people already do.
We can be a little more structured. First, for macros.tex aficionados, we'll use the command \notation to define a new symbol, so all the definitions can go in one place. For example,
\notation{trace}{\tau}
This defines the command \trace as a macro for \tau.
More importantly, it defines the paired command \traceDef, which is used to mark the definition site of this symbol, and which every occurrence of \trace unobtrusively links to.
For example, having written this,
A \emph{trace} $\trace$ is a sequence of states...
simply include \traceDef nearby:
A \traceDef\emph{trace} $\trace$ is a sequence of states...
Subsequent uses of \trace (even the one right after) will now contain links back to this part of the paper.
Doing this has benefits for authors too. The introduction of a new concept is now made explicit, which may help you consider if you're doing a "forward definition"; if you forget the definition, you get a compilation warning. Furthermore, paired with SyncTex, you can really zip around the paper.
For an example of this in action, I've annotated my most recent paper here.
The amount of effort was very low for the value – it's very much pay-as-you-go, and easy to do while proofreading. To prioritize, focus on important notations first (which readers will frequently have to refer back to), then obscure ones or those with a large distance to their definitions.
Design decisions
Why don't both commands take any parameters?
For \traceDef, it's so it can be placed anywhere, alongside what is written. To repeat the example from before:
A \traceDef\emph{trace} $\trace$ is a sequence of states...
On the other hand, \trace taking no argument may seem like a deficiency: how should we replace a \newcommand with parameters?
\newcommand*{\bigstep}[3]{#1\leadsto_{#2}#3}
% what's the \notation equivalent?
% a use
We define the relation \bigstep{e}{\trace}{v} as follows...
The reason is that we seldom want the entire term to become a link: it's possible we want to introduce notation for subterms, like the metavariable e.
My suggested way forward is to define notation for some essential symbol in the term, then use it in the definition of the term macro.
\notation{bigstepto}{\leadsto}
\newcommand*{\bigstep}[3]{#1\bigstepto_{#2}#3}
We define the relation \bigsteptoDef\bigstep{e}{\trace}{v} as follows...
This way, which portion becomes a link is always well-defined, and there is no problem with nesting notations.
Could we instrument \newcommand?
I briefly entertained the idea of instrumenting \newcommand to automate defining notations.
However, \newcommand is used for all kinds of things, not just definitions.
We would also have to handle the case of a command having parameters (see previous point).
Could we automatically link to the first use?
An early version of this defined a command that redefined itself after the first time it was used, so subsequent uses would link back to the first one. This seemed like a nice idea, based on the assumption that "forward definitions" should be avoided.
However, this can be fragile when used with figures, which may end up ordered before any given text on a page, and it is sometimes natural to defer a formal definition until after an intuitive use has been explained.
The current simpler design, relying on manual annotation of the definition site, seems more robust.
More use cases
It's sometimes useful to use the lower-level \notationlink and \notationtarget directly.
For example, say you typeset the names of inference rules in a special font.
\newcommand{\rulen}[1]{\ensuremath{{\bf \scriptstyle #1}}}
You can instrument it so that it adds a link, and define another variant for introducing a definition, which you then use in your inference rule.
\newcommand{\rulen}[1]{\notationlink{#1}{\ensuremath{{\bf \scriptstyle #1}}}}
\newcommand{\defrulen}[1]{\notationtarget{#1}{\ensuremath{{\bf \scriptstyle #1}}}}
If you have a mixfix judgment and want all the parts around the arguments to be links, adding an extra \notationlink is the easiest way to achieve this.
\notation{smodels}{\models}
\newcommand*{\bigstep}[3]{#1\smodels #2 \notationlink{smodels}{\leadsto} #3}