#49 Self-Education in PL - Ryan Brewer
Type Theory Forall
Ryan Brewer is a college dropout who has an incredible blog about PL, Category Theory and Logic. He better define his goal as making Formal Theory more accessible outside the ivory tower of academia, and easier to put into practice where it matters.
He has a couple of very interesting main projects, such as the first Cedille 2 Interpreter, Saber VM, and Arctic.
In this episode we will talk about all of his projects. His trajectory becoming self-taught in PL, compilers and Formal Methods, and he shares with us the wealth of resources he used to navigate this sea of knowledge. We also have a brief but heated discussion on the ethics of Science.
Links
- Ryan's Website
- Saber VM
- Arctic, which is built on top of Lustre
- Category Theory Wiki
Next Episodes
#48 Bell Labs - David MacQueen @ Type Theory Forall
π 2025-01-21 12:30 / β 02:10:12
#47 The History of LCF, ML and HOPE - David MacQueen @ Type Theory Forall
π 2025-01-07 13:00 / β 02:05:04
#46 Realizability, BHK, CPS Translation, Dialectica - Pierre-Marie PΓ©drot @ Type Theory Forall
π 2024-11-29 10:30 / β 01:03:36
#45 What is Type Theory and What Properties we Should Care About - Pierre-Marie PΓ©drot @ Type Theory Forall
π 2024-11-24 13:45 / β 01:21:41
#44 Theorem Prover Foundations, Lean4Lean, Metamath - Mario Carneiro @ Type Theory Forall
π 2024-11-06 22:00 / β 02:13:31