![Type Theory Forall artwork](https://is5-ssl.mzstatic.com/image/thumb/Podcasts124/v4/ed/de/43/edde43db-febe-b892-3a30-358ebe2e2c07/mza_16532267942080647912.png/100x100bb.jpg)
#39 Equality, Quotation, Bidirectional Type Checking - David Christiansen
Type Theory Forall
English - June 13, 2024 20:30 - 1 hour - 75.3 MB - ★★★★★ - 6 ratingsTechnology Science type theory programming languages academia Homepage Download Apple Podcasts Google Podcasts Overcast Castro Pocket Casts RSS feed
Previous Episode: #38 Haskell, Lean, Idris, and the Art of Writing - 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