#46 Realizability, BHK, CPS Translation, Dialectica - Pierre-Marie Pédrot - Type Theory Forall

Om avsnittet

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

#46 Realizability, BHK, CPS Translation, Dialectica - Pierre-Marie Pédrot

Om avsnittet

Links

Fler avsnitt

#64 PL Education in the Age of AI - Shriram Krishnamurthi

#63 Hack: Typing PHP at Facebook Scale - Julien Verlaguet

#62 Dependent Haskell - Vladislav Zavialov

#61 Zurihac Behind the Scenes - Farhad Mehta

#60 Conversations on Life, AI, and the PL Job Market - Pedro and Dan

#59 Category Theory and Inclusivity - Valeria de Paiva

#58 Constructivism and Computational Content - Andrej Bauer

#57 Compilers for Privacy-Preserving Computation, Category Theory, and Keeping a Good Rythm in your PhD - Raghav Malik

#56 Property Based Testing and PL Grad School Applications - Francille Zhuang

#55 The Death of OO, The Beauty of Scheme, BobKonf, and FunArch - Mike Sperber