In this episode we continue with our conversation with David MacQueen, he is an Emeritus Professor from the University of Chicago, and has worked at Bell Labs for 20 years.
Bell Labs began as the research and development section of the American Telephone and Telegraph company, aka AT&T, which originally hold exclusive hold of the telephone patent. Once that expired in the 1800s they needed to develop new technology to prove that it was still the best company, and hence Bell Labs was born.
Over the course of the years this fascinating institution has registered more than 26 thousand patents, among of which we have the transistor, the laser, the solar cell and communication satellites. Over the course of the last 88 years they were awarded a jaw dropping amount of 10 Nobel prizes and 5 Turing awards.
In this interview David MacQueen shares with us how was it like to work in such an incredible institution during it’s golden age. He shares insights about the technology, the space, the people, the management style, and much more!
Links
David's Website
David's Github
--------
2:10:12
#47 The History of LCF, ML and HOPE - David MacQueen
David MacQueen has worked at Bell Labs for around 20 years during it’s Golden Age. Professor at Chicago University for 23 years. He is one of the designers of SML, one of the fathers of HOPE the programming language that introduced the notion of Algebraic Datatypes.
So this interview was very special to me personally where I could get to hear all the stories about the dawn of Functional Programming as we know. And it is my great pleasure to have the honor to share it with you all.
Links
David's Website
David's Github
Luca Cardelli and the Early Evolution of ML
The History of SML
HOPE
SML Website
SML/NJ Website
SML/NJ Github
SML Family Website
In this episode Pierre-Marie Pédrot, one of the main Coq/Rocq developers joins us to talk about Krivine, Kleene and Gödel Realizability Models, how it relates to the BHK interpretation and CPS Translations, and how it was all already part of Gödel's work in Dialectica!
If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.com/typetheoryforall
Links
Pierre-Marie's Website
Pierre-Marie's PhD Thesis (Very nice read)
BHK Interpretation
Type Theory Forall website
Type Theory Forall discord
--------
1:03:36
#45 What is Type Theory and What Properties we Should Care About - Pierre-Marie Pédrot
In this episode Pierre-Marie Pédrot who is one of the main Coq/Rocq developers joins us to talk about what is Type Theory, what is Martin-Löf Type Theory, what are the properties we should care about in our type theory and why.
If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.com/typetheoryforall
Links
Pierre-Marie's Website
Type Theory Forall website
Type Theory Forall discord
--------
1:21:41
#44 Theorem Prover Foundations, Lean4Lean, Metamath - Mario Carneiro
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