A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs

Guillaume Allais, Robert Atkey, James Chapman +2

Almost every programming language's syntax includes a notion of binder and corresponding bound occurrences, along with the accompanying notions of $\alpha$-equivalence, capture-avoiding…