file:///home/cdo/src/sgl-paper/result/paper.pdf
Introduciton
Programs such as proof assistants, SMT solvers and compilers that operate on complex datat structures all require a representation of bound-variables. Many attempts have been made to formalize the semantics of variable binding, including category-theoretic models, Higher Order Abstract Syntax (HOAS), Nominal Techniques, De Bruijn Indices, first-order/nameful paradigms, and graphical representations.