"A Little Taste of Dependent Types" by David Christiansen
Strange Loop ConferenceYouTube ↗
Archive guide
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.