Stéphane Lescuyer. Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq. (Formalisation et developpement d'une tactique reflexive pour la demonstration automatique en coq). PhD thesis, University of Paris-Sud, Orsay, France, 2011. [doi]
Abstract is missing.