Type Theory Forall

Nov 29 2024 47 ep. 94 mins 223
Type Theory Forall Podcast artwork

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

  Technology  Science
RSS feed Share
Copy RSS


Subscribe on Podcast Addict


#46 Realizability, BHK, CPS Translation, Dialectica - Pierre-Marie Pédrot

Nov 29 2024 63 mins  
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 Pie

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

Nov 24 2024 81 mins  
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 webs

#44 Theorem Prover Foundations, Lean4Lean, Metamath - Mario Carneiro

Nov 06 2024 133 mins  
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 gi

#43 PL in the Industry and Summer Schools - Patrick and Eric

Sep 13 2024 61 mins  
In this episode Eric Bond and Patrick Lafontaine joins us to talk about the life in industry vs the life in academia. Eric is a PhD student at Michigan University under Max New, he works with some pretty cool esoteric cubical agda stuff. Before starting his PhD he has spent some time at the consultancy companies Two Six Technologies and 47 Degrees doing some cool functional program

#42 Distributed Systems, Microservices, and Choreographies - Fabrizio Montesi

Aug 29 2024 112 mins  
In this episode we talk with Fabrizio Montesi, a Full Professor at the University of South Denmark. He is one of the creators of the Jolie Programming Language, President of the Microservices Community and Author of the book 'Introduction to Choreographies'. In today’s episode we talk about the formal side of Distributed Sytems, session types, the calculi that model distributed s

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

Aug 15 2024 101 mins  
Satnam Singh has got incredible experience in both academia and industry. He has worked in Google, Facebook, Microsoft, Microsoft Research, Xilinx, etc. He has been a lecturer in Glasgow, Birmingham and University of California for a couple of years. He has worked with many interesting tools such Coq, Haskell, Verilog, Tensorflow. These days he works at Groq, applying FP to design

#40 Secure Voting - Joe Kiniry

Jul 15 2024 68 mins  
In this episode we go into a deep dive into the formal methods side of Voting systems, and for this nobody better than our guest: Joe Kiniry, A Principal Scientist at Galois, Principled CEO and Chief Scientist of Free & Fair, a Galois spin-out focused on high-assurance elections technologies and services. For the past 20 years Joe has worked tirelessly in designing, developing,

#39 Equality, Quotation, Bidirectional Type Checking - David Christiansen

Jun 13 2024 109 mins  
In this episode we continue our conversation with David Christiansen, he wrote the books Functional Programming in Lean and the Little Typer. He has also worked as the Executive Director of the Haskell Foundation, at Galois and did his PhD developing a bunch of cool stuff for Idris. In today’s episode we talk about the story behind writing The Little Typer together with Dan Fried

#38 Haskell, Lean, Idris, and the Art of Writing - David Christiansen

May 16 2024 115 mins  
In this episode we talk with David Christiansen, he wrote the books Functional Programming in Lean and the Little Typer. He has also worked as the Executive Director of the Haskell Foundation, at Galois and did his PhD developing a bunch of cool stuff for Idris. David is a super upbeat person and I feel that we could spend hundreds of hours talking about Functional Programming Writ

#37 Compilers, Staging, Futamura Projections - Guannan Wei

Mar 11 2024 113 mins  
In this episode we talk with Guannan Wei, from Purdue University. Guannan finished his PhD last year under Tiark Rompf, and is currently doing his Post-Doc with Tiark. Guannan has worked on a plethora of different compilers topics, and in this conversation we will talk about Staging, Futamura Projections, Symbolic Execution, Compiler Applications in Smart Contracts and Quantum Prog