30 subscribers
Go offline with the Player FM app!
Podcasts Worth a Listen
SPONSORED


#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.
If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.com/typetheoryforall
Links
91 episodes
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.
If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.com/typetheoryforall
Links
91 episodes
All episodes
×
1 #52 Why is Haskell so special - Lennart Augustsson 1:30:31


1 #50 The Expression Problem, Functional Pearls, Program Calculation - Wouter Swierstra 2:06:47

1 #49 Self-Education in PL - Ryan Brewer 2:23:47


1 #47 The History of LCF, ML and HOPE - David MacQueen 2:05:04

1 #46 Realizability, BHK, CPS Translation, Dialectica - Pierre-Marie Pédrot 1:03:36

1 #45 What is Type Theory and What Properties we Should Care About - Pierre-Marie Pédrot 1:21:41

1 #44 Theorem Prover Foundations, Lean4Lean, Metamath - Mario Carneiro 2:13:31

1 #43 PL in the Industry and Summer Schools - Patrick and Eric 1:01:30

1 #42 Distributed Systems, Microservices, and Choreographies - Fabrizio Montesi 1:52:49

1 #41 The Value of PL (and) Education - Satnam Singh 1:41:04


1 #39 Equality, Quotation, Bidirectional Type Checking - David Christiansen 1:49:42

1 #38 Haskell, Lean, Idris, and the Art of Writing - David Christiansen 1:55:58

1 #37 Compilers, Staging, Futamura Projections - Guannan Wei 1:53:20

1 #36 Behind the Person Behind this Podcast - Pedro Abreu 1:49:55

1 #35 Teika, Self-Education and F***ing Floating Points - Eduardo Rafael 1:21:29

1 #34 Foundations of Theorem Provers and Cedille2 - Andrew Marmaduke 1:28:27

1 #33 Z3 and Lean, the Spiritual Journey - Leo de Moura 2:05:07

1 #32 TyDe Systems - Jan de Muijnck-Hughes 1:41:23

1 #31 Discussing Problems in PL and Academia - Jan de Muijnck-Hughes 2:09:59

1 #30 Actors, GADTs and Burnout - Dan and Pedro 1:44:52

1 #29 Can PL theory make you a better software engineer? - Jimmy Koppel 1:24:19

1 #28 Formally Verifying Smart Contracts - Pruvendo 1:10:40

1 #27 Formalizing an OS: The seL4 - Gerwin Klein 1:58:40

1 #26 Mechanizing Modern Mathematics - Kevin Buzzard 2:15:31

1 #25 Formally Verifying the Tezos Codebase - Formal Land 1:01:32

1 #24 The History of Isabelle - Lawrence Paulson 1:38:02

1 #23 What is the SIGPLAN? - Jens Palsberg and Jonathan Aldrich 1:12:13

1 #22 Impredicativity, LEM, Realizability and more - Cody Roux 2:19:23

1 #21 Denotational Design - Conal Elliott 3:07:26

1 #20 Huaweii, String Diagrams, Game Semantics - Dan R. Ghica 1:37:28

1 #19 Experience Report: Learning Coq - Patrick and Supun 1:51:39

1 #18 Gödel's Incompleteness Theorems - Cody Roux 2:50:14

1 #17 The Lost Elegance of Computation - Conal Elliott 3:32:38

1 #16 Agda, K Axiom, HoTT, Rewrite Theory - Jesper Cockx 1:35:53

1 #15 Coq Projects, Agda, Idris, Kind - Nitin and Eric 1:17:36

1 #14 POPL, Parametricity, Scala, DOT - Nitin and Eric 56:30

1 #13 C/C++, Emacs, Haskell, and Coq. The Journey - John Wiegley 1:39:30

1 #12 Tenure, Sexism and ADHD - Talia Ringer 1:05:53

1 #11 FP, Monads, GHC, and beyond - Alejandro Serrano 1:07:12

1 #10 Classical Logic vs Intuitionistic Logic - Thorsten Altenkirch and Anupam Das 1:16:30


Welcome to Player FM!
Player FM is scanning the web for high-quality podcasts for you to enjoy right now. It's the best podcast app and works on Android, iPhone, and the web. Signup to sync subscriptions across devices.