Programs and Proofs — Dependent Typing as a Way to Structure Your Code
summary
An introduction to dependent types using Idris2 that explains how types can be treated as values and indexed by runtime values. It shows two simple examples including a formal proof that an optimization of a function preserves its behavior, and discusses how these proof-oriented techniques can inform development in languages without full dependent typing.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:51Dependent types examples
- 9:01Safe printf in Idris
- 11:52Dependent types history
- 14:23Constructive logic vs LEM
- 18:19Logic vs dependent types
- 24:40Formal typing and proofs
- 26:27Precise types prevent bugs
- 31:02Optimizing with dependent types
- 39:50Q&A
related talks
24mImperative Syntax for Dependent Types
19mIll-Typed Programs Don't Evaluate
47mType-Driven Development in Idris
12mIdris2-Table: Evaluating dependently-typed tables with... (Extended Abstract)
41mType-driven Development of Communicating Systems in Idris
39mDependent Type Driven Program Synthesis in Idris
18mDeveloping a Dependently Typed Language with Runtime Proof Search
43mIdris 2: Type-driven development of Idris