#44 Theorem Prover Foundations, Lean4Lean, Metamath - Mario Carneiro - Type Theory Forall

Om avsnittet

Mario Carneiro is the creator of Mathlib, Lean4Lean and Metamath0. He is currently doing his Postdoc at Chalmers University working on CakeML. In this episode we talk about foundations of theorem provers, type systems properties, semantics and interoperabilities.

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

#44 Theorem Prover Foundations, Lean4Lean, Metamath - Mario Carneiro

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