In this episode Pierre-Marrie Pédrot who is one of the main Coq/Rocq developers joins us to talk about what is Type Theory, what is Martin-Lof 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

• Pierre-Marie's Website
• Type Theory Forall website
• Type Theory Forall discord

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

• Lean4Lean github
• Metamath
• Metamath0
• Lean Foundations Discussion
• Large Elimination / Singleton Elimination
• Type Theory Forall website
• Type Theory Forall discord

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 programming and formal methods. Before that we were pals doing an internship at Galois, and even before that he finished his masters with Benjamin Delaware at Purdue, Patrick’s current advisor. Patrick has just returned from his internship at AWS in the automated reasoning team. So in this episode we talk about their research, their academic and industry experiences, how’s the industry looking like for opportunities in PL and all that.

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

• Type Theory Forall website
• Type Theory Forall discord

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 systems, their type systems, their Curry-Howard correspondences, and all the main ideas around these concepts.

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

• Fabrizio's Website
• Fabrizio's Linkedin
• Fabrizio's X / Twitter
• Fabrizio's Mastodon
• Fabrizio's Youtube
• Jolie's Website

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 silicon for machine learning. In this episode we talk about the value of specification, the current state of academia, gaming the metrics, functional programming in hardware, bullying, among other things.

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

• Personal Website
• Satnam's X
• Groq

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, supporting and auditing all kinds of voting systems for different private parties and government parties.

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

Broken Ballots

Joe Website

Galois website

SAW

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 Friedman, and we get more technical by talking about Equality, Bidirectional Type Checking, Quotation and Quasi Quotation.

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

• David's Website
• David's X
• Lean Zulip Chat
• Truth of a proposition, evidence of a judgement, validity of a proof

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 Writing and Dependent Types, and we still wouldn’t run out of topics!

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