@article{ZILIANI_2015,
    doi = {10.1017/s0956796815000118},
    url = {https://doi.org/10.1017%2Fs0956796815000118},
    year = {2015},
    publisher = {Cambridge University Press ({CUP})},
    volume = {25},
    author = {BETA ZILIANI and DEREK DREYER and NEELAKANTAN R. KRISHNASWAMI and ALEKSANDAR NANEVSKI and VIKTOR VAFEIADIS},
    title = {Mtac: A monad for typed tactic programming in Coq},
    journal = {Journal of Functional Programming}
}

@article{ZILIANI_2015, doi = {10.1017/s0956796815000118}, url = {https://doi.org/10.1017%2Fs0956796815000118}, year = {2015}, publisher = {Cambridge University Press ({CUP})}, volume = {25}, author = {BETA ZILIANI and DEREK DREYER and NEELAKANTAN R. KRISHNASWAMI and ALEKSANDAR NANEVSKI and VIKTOR VAFEIADIS}, title = {Mtac: A monad for typed tactic programming in Coq}, journal = {Journal of Functional Programming} }