@article{Gonthier:2011:MAH:2034574.2034798,
    Address = {New York, NY, USA},
    Author = {Gonthier, Georges and Ziliani, Beta and Nanevski, Aleksandar and Dreyer, Derek},
    File = {How to make ad hoc proof automation less ad hoc - Gonthier, Ziliani, Nanevski, Dreyer (0) (0) - a - a - j.pdf},
    ISSN = {0362-1340},
    Journal = {SIGPLAN Not.},
    Keywords = {canonical structures, coq, custom proof automation, hoare type theory, interactive theorem proving, tactics, type classes},
    Month = {September},
    Number = {9},
    Pages = {163--175},
    Publisher = {ACM},
    Title = {How to make ad hoc proof automation less ad hoc},
    URL = {http://doi.acm.org/10.1145/2034574.2034798},
    Volume = {46},
    Year = {2011},
    acmid = {2034798},
    bdsk-url-1 = {http://doi.acm.org/10.1145/2034574.2034798},
    bdsk-url-2 = {http://dx.doi.org/10.1145/2034574.2034798},
    date-added = {2013-01-30 17:39:41 +0000},
    date-modified = {2013-01-30 17:39:41 +0000},
    file-2 = {How to make ad hoc proof automation less ad hoc - Gonthier, Ziliani, Nanevski, Dreyer (1) (0) - a - a - j.pdf},
    file-3 = {How to make ad hoc proof automation less ad hoc - Gonthier, Ziliani, Nanevski, Dreyer (2) (0) - a - a - j.pdf},
    issue_date = {September 2011},
    numpages = {13},
    doi = {10.1145/2034574.2034798}
}

@article{Gonthier:2011:MAH:2034574.2034798, Address = {New York, NY, USA}, Author = {Gonthier, Georges and Ziliani, Beta and Nanevski, Aleksandar and Dreyer, Derek}, File = {How to make ad hoc proof automation less ad hoc - Gonthier, Ziliani, Nanevski, Dreyer (0) (0) - a - a - j.pdf}, ISSN = {0362-1340}, Journal = {SIGPLAN Not.}, Keywords = {canonical structures, coq, custom proof automation, hoare type theory, interactive theorem proving, tactics, type classes}, Month = {September}, Number = {9}, Pages = {163--175}, Publisher = {ACM}, Title = {How to make ad hoc proof automation less ad hoc}, URL = {http://doi.acm.org/10.1145/2034574.2034798}, Volume = {46}, Year = {2011}, acmid = {2034798}, bdsk-url-1 = {http://doi.acm.org/10.1145/2034574.2034798}, bdsk-url-2 = {http://dx.doi.org/10.1145/2034574.2034798}, date-added = {2013-01-30 17:39:41 +0000}, date-modified = {2013-01-30 17:39:41 +0000}, file-2 = {How to make ad hoc proof automation less ad hoc - Gonthier, Ziliani, Nanevski, Dreyer (1) (0) - a - a - j.pdf}, file-3 = {How to make ad hoc proof automation less ad hoc - Gonthier, Ziliani, Nanevski, Dreyer (2) (0) - a - a - j.pdf}, issue_date = {September 2011}, numpages = {13}, doi = {10.1145/2034574.2034798} }