Technology
**Type Theory Forall**

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

Latest Episodes:

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

Show notes

Andrew Marmaduke is a PhD Candidate from the University of Iowa, he works under Aaron Stump and has been working on revamping the theorem prover Cedille 2. In this episode we tackle fundamental questions about the foundations of the theorem provers, Cedille and Cedille 2.

If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.com/typetheoryforall

Links

#33 Z3 and Lean, the Spiritual Journey - Leo de Moura Sep 09, 2023

Show notes

Not satisfied with implementing one of the most popular automated theorem provers, Z3, Leo de Moura also tackles another extremely hard problem in our field and implements a brand new interactive theorem prover from scratch, Lean. In this episode we dive into the mind and philosophy of this man.

If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.com/typetheoryforall

Links

#32 TyDe Systems - Jan de Muijnck-Hughes Jul 22, 2023

Show notes

In this episode we continue our conversation with Jan de Muijnck-Hughes a Research Associate at Glasgow University. He works using all sorts of fancy type systems mostly targeted for hardware specification, particularly with the aid of the theorem prover Idris. This episode we start by talking a little about Impostor Syndrome in academia and how he has learned to cope with it and then we dive deeper into the technicalities of his research, in particular his philosophy on Type Directed Design of Systems. We talk about Session Types, Graded Types, Quantitative types, etc.

Don't forget to join our new discord channel!

If you like our show please consider donating any amount at ko-fi.

Links

Project Pages

Cool People

Software

#31 Discussing Problems in PL and Academia - Jan de Muijnck-Hughes Jul 13, 2023

Show notes

In this episode we have a deep conversation with Jan de Muijnck-Hughes, talks about all the cool research he has done with idris, hardware and different kinds of interesting type systems such as session types, quantitative types and graded types. In the second half we discuss all the different kinds of problems that has been going on in PL academia lately and what we can do as a community to address those issues.

Also, we have a discord channel now, join us!

If you like our show please consider donating any amount at ko-fi.

Errata:

Jan mentions 'Jeff Foster' when, in fact, he meant Nate Foster
This is the SIGCOMM 'Call': https://sigcomm.quest/
Felinne Hermans did her PhD at Eindhoven and not Delft

Links

#29 Can PL theory make you a better software engineer? - Jimmy Koppel Apr 09, 2023

Show notes

Jimmy Koppel, got his PhD at MIT and found the Mirdin Company, where he teaches engineers to write better code! In this interview we talk about how to make better code, how the knowledge of computer science theory and programming languages can help engineers to achieve that, and much more!

Links

Newsletters discussed in the show

#28 Formally Verifying Smart Contracts - Pruvendo Feb 15, 2023

Show notes

In this episode we host another company that does formal method in the context of the Everscale Blockchain, and Solidity smart contracts. How and why they use formal methods in this context? Who are their clients? What are the caveats?

Links

#27 Formalizing an OS: The seL4 - Gerwin Klein Feb 04, 2023

Show notes

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

#26 Mechanizing Modern Mathematics - Kevin Buzzard Jan 16, 2023

Show notes

Kevin Buzzard has been very passionate spreading the word among mathematicians to use theorem provers mechanize theorems of modern mathematics. In this conversation we will talk about his vision in teaching undergrads to use the Lean theorem prover, what is the Xena Project and Mathlib, his view of how theorem provers can change the way we do mathematics, and much more!

Links

#25 Formally Verifying the Tezos Codebase - Formal Land Nov 21, 2022

Show notes

In this episode we partner with Formal Land, a company that works in formally verifying the Tezos codebase! I have worked with them in the past developing new features to their source-to-source compiler CoqOfOcaml. In this episode we talk about their work with Tezos and how their techniques are applicable to other codebases as well! For this we talk with Formal Land founder Guillaume Claret and the proof engineers Daniel Hilst and Pierre Vial.