Powered by RND
PodcastsTechnologieType Theory Forall
Luister naar Type Theory Forall in de app
Luister naar Type Theory Forall in de app
(2.067)(250 021)
Favorieten opslaan
Wekker
Slaaptimer

Type Theory Forall

Podcast Type Theory Forall
Pedro Abreu
An accessible podcast about Type Theory, Programming Languages Research and related topics.

Beschikbare afleveringen

5 van 49
  • #48 Bell Labs - David MacQueen
    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
    --------  
    2:05:04
  • #46 Realizability, BHK, CPS Translation, Dialectica - Pierre-Marie Pédrot
    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
    --------  
    2:13:31

Meer Technologie podcasts

Over Type Theory Forall

An accessible podcast about Type Theory, Programming Languages Research and related topics.
Podcast website

Luister naar Type Theory Forall, Bright Podcast en vele andere podcasts van over de hele wereld met de radio.net-app

Ontvang de gratis radio.net app

  • Zenders en podcasts om te bookmarken
  • Streamen via Wi-Fi of Bluetooth
  • Ondersteunt Carplay & Android Auto
  • Veel andere app-functies

Type Theory Forall: Podcasts in familie

Social
v7.8.0 | © 2007-2025 radio.de GmbH
Generated: 2/19/2025 - 5:23:32 PM