Kaiser, J.-O., Ziliani, B., Krebbers, R., Régis-Gianas, Y., & Dreyer, D. (2018). Mtac2:Typed Tactics for Backward Reasoning in Coq. Proceedings of the ACM on Programming Languages, 2(ICFP): 78. doi:10.1145/3236773.