What are Dependent Types

on YouTube ↗11m

" summary

Claims that dependent types can encode arbitrary mathematical propositions and that a type checker enforces those properties statically. Demonstrations include inductive naturals, an even(n) predicate, and encoding notions like sorted lists, prime numbers, or a function that returns the max; proofs appear as types, not booleans. The talk shows actual tooling: inductive definitions, pattern matching, a tactic scripting layer and the Curry Howard isomorphism connecting programs and proofs.

AI-written summary · about

" chapters (5)

1. 0:00Start
2. 1:41Lambda Calculus
3. 3:04Type Operators
4. 4:51Function Types
5. 6:19Inductive Datatype

" related talks

• 56mIdris: Programming with Dependent TypesEdwin Brady · Code Mesh 2013
• 01h 44mAn Introduction to Natural DeductionLyle Kopnicky · LambdaConf 2019
• 39mA Little Taste of Dependent TypesDavid Christiansen · Strange Loop 2018
• 35mProof Theory Impressionism: Blurring the Curry-Howard LineDan Pittman · Strange Loop 2018
• 41mWar Time Proofs and Futuristic ProgramsValeria de Paiva · Strange Loop 2023
• 01h 04mThe Leibniz Library and Applied Propositions as TypesAlexander Konovalov · LambdaConf 2018
• 22mA Certifying Proof Assistant for Synthetic Mathematics in LeanWojciech Nawrocki, Joseph Hua, Mario Carneiro, Yiming Xu, Spencer Woolfson, Shuge Rong, Sina Hazratpour, Steve Awodey · CPP 2026
• 26m(...) How to turn (Liquid) Haskell into a theorem proverNiki Vazou · Lambda Days 2017