Type Theory Forall

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 Links 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 Links 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 Links Broken Ballots Joe Website Galois website SAW

David Christiansen, former Executive Director of the Haskell Foundation, talks about writing The Little Typer, Equality, Bidirectional Type Checking, and Quotation with the host. They explore the challenges of book reprints, bi-directional type checking, macro implementation, and Lean macros. Technical discourse on content levels and audience interaction, with insights on normalization by evaluation and personal anecdotes.

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

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 Programming. Towards the end of the episode we also talk about his application experiences for the position of a Professorship in the US an a few other contries. If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.com/typetheoryforall Links Guannan's Website @guannanwei on X

In this episode we celebrate 3 years of existence of this podcast by reflecting on the journey so far, what is my philosophy, how do I approach the interviews, my overall goals for the show, and some of our plans for the future. In order to achieve this, I first take a detour and tell you a little more about my personal history, and my carreer in type theory and programming languages. If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.com/typetheoryforall

In this episode we talk with Eduardo Rafael. He is self-thaught programming languages enthusiast, youtuber, twitch streamer, multi-skilled programmer that has worked in different aspects of computer science such as PL, operating systems, blockchain, and many other stuff. In this conversation we talk about his experience as a developer and hacker that didn’t follow the conventional paths of going to school and what are the strategies to navigate the vast ocean of knowledge without guidance of teachers or institutions. If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.com/typetheoryforall Links Eduardo's Twitter Eduardo's Twitch Eduardo's Youtube Feynman Algorithm

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 Andrew's Website AndrasKovacs' Smalltt Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality Impredicative Encodings of (Higher) Inductive Types

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 Leo's Website Lean Z3 The Church of Logic Podcast