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

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. Some links: 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!

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. 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.

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

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 Jan's website Jan's twitter Jan's mastodon Writing and Speaking with Style Artifact Eval Andrej Bauer: Formalising Invisible Mathematics Hedy language (Felienne Hermans) Hermans' Inaugural Lecture on making PL human and inclusive Epistemic Injustice Richard Eisenberg interview 'Software Foundations' but in Agda 'System F for Fun & Profit' Reviewing Project Pages https://dsbd-appcontrol.github.io/ https://border-patrol.github.io/ Cool People Rachit Nigam Clement Pit-Claudel Software Idris Language Biblio

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 Jan's website Jan's twitter Jan's mastodon Writing and Speaking with Style Artifact Eval Andrej Bauer: Formalising Invisible Mathematics Hedy language (Felienne Hermans) Hermans' Inaugural Lecture on making PL human and inclusive Epistemic Injustice Richard Eisenberg interview 'Software Foundations' but in Agda 'System F for Fun & Profit' Reviewing Project Pages https://dsbd-appcontrol.github.io/ https://border-patrol.github.io/ Cool People Rachit Nigam Clement Pit-Claudel Software Idris Language Biblio

In this episode we have over Dan Plyukhin, a PhD Candidate from the University of Illinois Urbana-Champaign. We talk about Dan’s research is in the field of parallelism, more specifically garbage collection in the presence of actors. Then we also talk about Pedro's research on translating GADTs from OCaml to Coq, and the burnout process that lead him to take 10 months off from his PhD to be with his family back in Brazil. Links Dan's Personal Website Twitter: @dplyukhn