Koenig, J. Coqrel: a binary logical relations library for the Coq proof assistant [Computer software]. https://github.com/CertiKOS/coqrel