Dependent Types with David Christiansen

https://is1-ssl.mzstatic.com/image/thumb/Podcasts116/v4/90/bf/e9/90bfe928-e60b-d3ae-1a9b-d8675ebf6fb1/mza_2008178507985519125.jpg/600x600bb.jpg

Functional Futures

Serokell

12 episodes

6 days ago

Functional Futures is a podcast where we interview people that are building the future of functional programming. From compiler developers juggling parsers, lexers, and type theory to software developers working on industry-grade libraries and codebases, we have something for the taste of every FP enthusiast out there.

Science

RSS

All content for Functional Futures is the property of Serokell and is served directly from their servers with no modification, redirects, or rehosting. The podcast is not affiliated with or endorsed by Podjoint in any way.

Science

https://d3t3ozftmdmh3i.cloudfront.net/production/podcast_uploaded_nologo/20555440/20555440-1642688904194-930fe19d36731.jpg

Dependent Types with David Christiansen

Functional Futures

1 hour 46 minutes 34 seconds

3 years ago

Dependent Types with David Christiansen

In this month’s episode of Functional Futures, our guest is David Christiansen, the executive director of the Haskell Foundation, a contributor to a number of dependently typed languages, and a dependent type advocate that has managed to introduce many people to the topic today through his work, talks, and texts. In the episode, we cover topics such as dependent types, theorem proving, metaprogramming, and many more.
We also discuss the book David co-authored with Daniel P. Friedman, The Little Typer, and his current work in progress: Functional Programming in Lean.

Get FP merch that doesn't suck. 👇
https://shop.serokell.io/

David's books: The Little Types – https://mitpress.mit.edu/9780262536431/the-little-typer/
Functional Programming in Lean – https://leanprover.github.io/functional_programming_in_lean/

Follow on social media:
https://twitter.com/d_christiansen
https://twitter.com/serokell

Learn more about us: https://serokell.io/