In this episode Pierre-Marie Pédrot, one of the main Coq/Rocq developers joins us to talk about Krivine, Kleene and Gödel Realizability Models, how it relates to the BHK interpretation and CPS Translations, and how it was all already part of Gödel's work in Dialectica!

If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.com/typetheoryforall

Links

• Pierre-Marie's Website
• Pierre-Marie's PhD Thesis (Very nice read)
• BHK Interpretation
• Type Theory Forall website
• Type Theory Forall discord