Compiling contextual objects
Francisco Ferreira, Stefan Monnier, Brigitte Pientka · 2013
Binders in data-structures representing code or proofs can be represented in a variety of ways, from low-level first-order representations such as de Bruijn indices to higher-order abstract syntax (HOAS), with nominal logic somewhere in-between.