A Walk-through of Computational Reflection in Coq

November Boston Haskell Meetup @ ThoughBot

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.

https://www.meetup.com/Boston-Haskell/events/244608020/