Type Theory Forall

Andrej Bauer has done his PhD at CMU under Dana Scott, and he stands right on the edge between mathematics and computer science. During our conversation it just feels that he can just go on in depth about any topic remotely related to Type Theory and Programming Languages.

Andrej is the person who organized for the The Proof Assistants stack exchange. He has an incredible blog that’s always a great resource to learn Type Theory and Programming Languages Theory. He also has an incredible series of summer school lectures on effect handlers.

But more specifically today we talk about Constructivism, Dialectica, Effect Handlers and AI. I’m sure you guys are gonna love it!

Links

Andrej's Website

Andrej's Blog

Raghav Malik, has just defended his PhD on the topic of compilers for privacy-preserving computation, and that's a good chunk of our conversation.

He has also spent some years in grad school going down the rabbit hole to actually learn Category Theory in depth and from first principles, so I was deieing to ask him if category theory is really all that to learn the foundations of PL. In other words, does learning category theory really make you a better PL researcher?

Then, of course, I wouldn’t finish this episode without asking him how he coped with Mental Health during his PhD Journey.

Links

Raghav's Website

TTFA Patreon
TTFA Merch Store
TTFA Ko-Fi

Francille Zhuang is an undergrad at Purdue University and has been doing research with Benjamin Delaware and Patrick Lafontaine. In this episode we talk about her early research experiences on Property Based Testing, and we go through all the necessary information for applying for graduate school in Programming Languages in the US.

Links

Francille's LinkedIn

TTFA Mentorship Program

TTFA Merch Store

TTFA Patreon

TTFA Ko-Fi

Mike Sperber is the CEO of Active Group, a company designed for Counseling, Development and Training in functional programming. He is a co-organizer of Bob Konf and FunArch, the Co-founder of the leading german blog on functional programming. Member of the Editorial Board of the JFP. Part of the R6RS, the 6th revised report on the Algorithmic Language Scheme.

In our conversation we talk about C, Lisp, Emacs Lisp, Scheme and his involvement with the R6RS. His views on mathematics and formal methods as languages, his views on the use of Functional Programming in the Industry, his thoughts of how Object Oriented Programming is dead. Macros, hygienic macros and much more!

We also talk about BobKonf and FunArch as amazing confereces on Functional Programming and their design and archtechture. BobKonf currently has a call for talks open and goes until november 17th.

Consider supporting the show!

TTFA Patreon

One time donations

Merch Store

Links

Mike's Website

Bob Konf

FunArch

Functional Programming Blog

TTFA Graduate Mentorship

Philip Wadler is a well known, celebrated and recognized researcher in the field especially for his unique ability to explain complex ideas in a simple and elegant way. He got his Bachelor in 1977 at Stanford, his Masters in 1979 and his PhD in 1984 both at CMU. In 2023, he was awarded the distinguished honor of being elected a Fellow of the Royal Society, joining the ranks of scientific greats such as Isaac Newton and Charles Darwin.

Wadler describes himself as someone who likes to bring theory into practice, and practice into theory. In this episode, we talk about his prolific research, the story behind Monads and Type Classes, Category Theory and Homotopy Type Theory.

Throughout our conversation, in response to my eagerness to understand the philosophy and method behind his remarkable papers, he repeatedly emphasizes that the whole point of science is clearly communicating ideas so that others can build upon them.

Links

Wadler's Website
Ullman's Advising Students For Success

Grad School Mentorship
Consider contributing to this show through our ko-fi!