
Sign up to save your podcasts
Or


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
 By Pedro Abreu
By Pedro Abreu4.8
1313 ratings
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

380 Listeners

523 Listeners

290 Listeners

188 Listeners

4,147 Listeners

19 Listeners

491 Listeners

72 Listeners

13 Listeners

27 Listeners

3,095 Listeners

59 Listeners

194 Listeners

497 Listeners