A Little Taste of Dependent Types: David Christiansen
Strange Loop Conference · Talk · YouTube title: "A Little Taste of Dependent Types" by David Christiansen
Why it's here
Recommended as an approachable introduction to dependent types and a preview of what The Little Typer covers.
What it covers
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.