
Sign up to save your podcasts
Or


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
By Pedro Abreu4.8
1313 ratings
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

383 Listeners

530 Listeners

288 Listeners

190 Listeners

4,175 Listeners

19 Listeners

505 Listeners

72 Listeners

13 Listeners

29 Listeners

3,070 Listeners

63 Listeners

182 Listeners

474 Listeners