Hammer for Coq: Automation for Dependent Type Theory. - Czajka, Łukasz; Kaliszyk, Cezary (Journal of Automated Reasoning, 2018)