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/