Gregory Malecha presents techniques for computational reflection in the Coq proof assistant. Computational reflection is a proof technique that makes use of programs written within the language of the proof assistant itself, rather than a meta-language.