Przejdź do trybu offline z Player FM !
#44 Theorem Prover Foundations, Lean4Lean, Metamath - Mario Carneiro
Manage episode 448843726 series 2951423
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. It was an absolutely amazing episode and I’m sure you guys will love it!
Links
Lean4Lean github Metamath Metamath0 Lean Foundations Discussion Large Elimination / Singleton Elimination
83 odcinków
Manage episode 448843726 series 2951423
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. It was an absolutely amazing episode and I’m sure you guys will love it!
Links
Lean4Lean github Metamath Metamath0 Lean Foundations Discussion Large Elimination / Singleton Elimination
83 odcinków
كل الحلقات
×Zapraszamy w Player FM
Odtwarzacz FM skanuje sieć w poszukiwaniu wysokiej jakości podcastów, abyś mógł się nią cieszyć już teraz. To najlepsza aplikacja do podcastów, działająca na Androidzie, iPhonie i Internecie. Zarejestruj się, aby zsynchronizować subskrypcje na różnych urządzeniach.