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

Type Theory Forall
06/11/2024 2h 13min
#44 Theorem Prover Foundations, Lean4Lean, Metamath - Mario Carneiro

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

Descargar episodio Ver en sitio original

Episode Synopsis



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
Links

Lean4Lean github
Metamath
Metamath0
Lean Foundations Discussion
Large Elimination / Singleton Elimination
Type Theory Forall website
Type Theory Forall discord




More episodes of the podcast Type Theory Forall

#57 Compilers for Privacy-Preserving Computation, Category Theory, and Keeping a Good Rythm in your PhD - Raghav Malik 06/12/2025
#56 Property Based Testing and PL Grad School Applications - Francille Zhuang 17/11/2025
#55 The Death of OO, The Beauty of Scheme, BobKonf, and FunArch - Mike Sperber 27/10/2025
#54 The Goal of Science is to Communicate Ideas! - Philip Wadler 29/09/2025
#53 RustBelt, Iris, and the Art of Writing - Derek Dreyer 27/08/2025
#52 Why is Haskell so special - Lennart Augustsson 10/07/2025
#51 s/Coq/Rocq - Nicolas Tabareau 04/06/2025
#50 The Expression Problem, Functional Pearls, Program Calculation - Wouter Swierstra 14/05/2025
#49 Self-Education in PL - Ryan Brewer 14/03/2025
#48 Bell Labs - David MacQueen 21/01/2025
© 2003-2025 ZARZA | AHEAD OF OUR TIME
privacy policy
In God we trust In God we trust
PreSales Questions? Click Here
or call our toll-free line at +1-888-5002068 Miami, Florida, USA