Nada Amin and Tiark Rompf. 2017. “Type soundness proofs with definitional interpreters.” In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, Pp. 666–679. ACM.