Blanchette, J. C., Popescu, A., & Traytel, D. (2017). Soundness and Completeness Proofs by Coinductive Methods. Journal of Automated Reasoning, 58(1), 149-179. doi: 10.1007/s10817-016-9391-3.