Timany, A., Krebbers, R., Dreyer, D., & Birkedal, L. (2024). A Logical Approach to Type Soundness. Journal of the ACM, 71(6): 40, pp. 1-75. doi:10.1145/3676954.