@article{GONTHIER_2013,
    doi = {10.1017/s0956796813000051},
    url = {https://doi.org/10.1017%2Fs0956796813000051},
    year = {2013},
    month = {jul},
    publisher = {Cambridge University Press ({CUP})},
    volume = {23},
    number = {4},
    pages = {357--401},
    author = {GEORGES GONTHIER and BETA ZILIANI and ALEKSANDAR NANEVSKI and DEREK DREYER},
    title = {How to make ad hoc proof automation less ad hoc},
    journal = {Journal of Functional Programming}
}

@article{GONTHIER_2013, doi = {10.1017/s0956796813000051}, url = {https://doi.org/10.1017%2Fs0956796813000051}, year = {2013}, month = {jul}, publisher = {Cambridge University Press ({CUP})}, volume = {23}, number = {4}, pages = {357--401}, author = {GEORGES GONTHIER and BETA ZILIANI and ALEKSANDAR NANEVSKI and DEREK DREYER}, title = {How to make ad hoc proof automation less ad hoc}, journal = {Journal of Functional Programming} }