Jan-Oliver Kaiser, Beta Ziliani, Robbert Krebbers, Yann Régis-Gianas, Derek Dreyer
Mtac2: typed tactics for backward reasoning in Coq
ICFP, 2018.
@article{ICFP-2018-KaiserZKRD, author = "Jan-Oliver Kaiser and Beta Ziliani and Robbert Krebbers and Yann Régis-Gianas and Derek Dreyer", doi = "10.1145/3236773", journal = "{Proceedings of the ACM on Programming Languages}", number = "ICFP", pages = "31", title = "{Mtac2: typed tactics for backward reasoning in Coq}", volume = 2, year = 2018, }