#37 Compilers, Staging, Futamura Projections March 11th 2024
Guannan Wei

#36 Behind the Person Behind this Podcast Dec 26th 2023
Pedro Abreu

#35 Teika, Self-Education and F***ing Floating Points Dec 04th 2023
Eduardo Rafael

#34 Foundations of Theorem Provers and Cedille2 Oct 16th 2023
Andrew Marmaduke

#33 Z3 and Lean, the Spiritual Journey Sep 9th 2023
Leo de Moura

#32 TyDe Systems July 22th 2023
Jan de Muijnck-Hughes

#31 Discussing Problems in PL and Academia July 13th 2023
Jan de Muijnck-Hughes

#30 Actors, GADTs and Burnout May 30th 2023
Dan and Pedro

#29 Can PL theory make you a better software engineer? April 9th 2023
Jimmy Koppel

#28 Formally Verifying Smart Contracts February 15th 2023
Pruvendo

#27 Formalizing an OS: The seL4 February 4th 2023
Gerwin Klein

In this episode talk with Gerwin Klein about the formal verification of the microkernel seL4 which was done using Isabelle at NICTA / Data61 in Australia. We also talk a little about his PhD Project veryfing a piece of the Java Virtual Machine.

Links

Download .mp3 (80.5M)
Tweet

#26 Mechanizing Modern Mathematics January 16th 2023
Kevin Buzzard

#25 Formally Verifying the Tezos Codebase November 21st 2022
Formal Land

#24 The History of Isabelle October 6th 2022
Lawrence Paulson

#23 What is the SIGPLAN? September 23th 2022
Jens Palsberg and Jonathan Aldrich

#22 Impredicativity, LEM, Realizability and more August 12th 2022
Cody Roux

#21 Denotational Design August 4th 2022
Conal Elliott

#20 Huaweii, String Diagrams, Game Semantics June 27th 2022
Dan R. Ghica

#19 Experience Report: Learning Coq June 4th 2022
Patrick and Supun

#18 Gödel's Incompleteness Theorems May 19th 2022
Cody Roux

#17 The Lost Elegance of Computation May 9th 2022
Conal Elliott

#16 Agda, K Axiom, HoTT, Rewrite Theory April 2nd 2022
Jesper Cockx

#15 Coq Projects, Agda, Idris, Kind March 27th 2022
Nitin and Eric

#14 POPL, Parametricity, Scala, DOT February 12th 2022
Nitin and Eric

#13 C/C++, Emacs, Haskell, and Coq. The Journey December 23rd 2021
John Wiegley

#12 Tenure, Sexism and ADHD November 10th 2021
Talia Ringer

#11 FP, Monads, GHC, and beyond October 4th 2021
Alejandro Serrano

#10 Classical Logic vs Intuitionistic Logic July 15th 2021
Thorsten Altenkirch and Anupam Das

#9 Logic and Proof Theory May 28th 2021
Anupam Das

#8 Cedille May 10th 2021
Chris Jenkins

#7 Hacking Isabelle's Internals April 15th 2021
Daniel Matichuk

#6 All The Dumb Questions on Gradual Types March 29th 2021
Zeina Migeed

#5 The History of Coq'Art February 27th 2021
Yves Bertot

#4 Theorem Provers, Functional Programming and Companies February 15th 2021
Eric Bond

#3 ML for PL and Mental Health February 1st 2021
Dan Zheng

#2 Grad School Life January 10th 2021
Rajan Walia and John Sarracino

#1 What is PL research? December 23rd 2020
Prof. Ben Delaware

#0 Cool Internships in PL December 14th 2020
Believe or not there are quite a few companies interested in Programming Languages Research.