Ziliani, B., Dreyer, D., Krishnaswami, N., Nanevski, A., & Vafeiadis, V. (2013). Mtac: A Monad for Typed Tactic Programming in Coq. In ICFP'13 (pp. 377-390). New York, NY: ACM. doi:10.1145/2500365.2500579.