HackerTube / Video
"A Little Taste of Dependent Types" by David Christiansen
Strange Loop Conference
David Christiansen gives a Strange Loop 2018 introduction to dependent types, where one language serves for both compile-time and run-time code and programs unite with proofs. It draws on his book The Little Typer.
Recommended as an approachable introduction to dependent types and a preview of what The Little Typer covers.
3 Hacker News mentions · 2018–2023