@article{Czajka:2018:HCA:3230162.3230182,
    Address = {Berlin, Heidelberg},
    Author = {Czajka, {\L}ukasz and Kaliszyk, Cezary},
    File = {lcck-jar18 (0) (0) - a - a - m.pdf},
    ISSN = {0168-7433},
    Journal = {J. Autom. Reason.},
    Keywords = {calculus of inductive constructions, Coq, hammer, proof automation, readme},
    Month = {June},
    Number = {1-4},
    Pages = {423--453},
    Publisher = {Springer-Verlag},
    Title = {Hammer for Coq: Automation for Dependent Type Theory},
    URL = {https://doi.org/10.1007/s10817-018-9458-4},
    Volume = {61},
    Year = {2018},
    acmid = {3230182},
    bdsk-url-1 = {https://doi.org/10.1007/s10817-018-9458-4},
    date-added = {2018-10-22 09:41:00 +0000},
    date-modified = {2019-03-21 20:12:20 +0100},
    issue_date = {June 2018},
    numpages = {31},
    doi = {10.1007/s10817-018-9458-4}
}

@article{Czajka:2018:HCA:3230162.3230182, Address = {Berlin, Heidelberg}, Author = {Czajka, {\L}ukasz and Kaliszyk, Cezary}, File = {lcck-jar18 (0) (0) - a - a - m.pdf}, ISSN = {0168-7433}, Journal = {J. Autom. Reason.}, Keywords = {calculus of inductive constructions, Coq, hammer, proof automation, readme}, Month = {June}, Number = {1-4}, Pages = {423--453}, Publisher = {Springer-Verlag}, Title = {Hammer for Coq: Automation for Dependent Type Theory}, URL = {https://doi.org/10.1007/s10817-018-9458-4}, Volume = {61}, Year = {2018}, acmid = {3230182}, bdsk-url-1 = {https://doi.org/10.1007/s10817-018-9458-4}, date-added = {2018-10-22 09:41:00 +0000}, date-modified = {2019-03-21 20:12:20 +0100}, issue_date = {June 2018}, numpages = {31}, doi = {10.1007/s10817-018-9458-4} }