Propositional Equality for Gradual Dependently Typed Programming

on YouTube ↗16m

" summary

A gradual dependently-typed language is implemented that adds a propositional equality whose proofs carry witnesses (each proof pairs an equality with a term at least as precise as both sides), so imprecise proofs like ? reduce to a witness = composition of X and Y and collapse to error when X and Y are inconsistent (example: buggy quicksort maps 989 to 89 and ? : 2=3 reduces to error). Composition is an internal language construct that defers checks for neutral terms, preserves extensional equivalence, and the paper proves type safety, conservative embedding of CIC, weak canonicity, and the gradual guarantees.

AI-written summary · about

" chapters (13)

1. 0:00Intro
2. 0:11Research Questions
3. 1:13A Buggy Quicksort
4. 2:10Adding the Spec To the Types (with the magic of dependent types)
5. 2:50Dependent Types Catch the Bug?
6. 5:12Gradual Types To The Rescue?
7. 5:32Imprecision has Dynamic Semantics
8. 7:00Review: Threesomes and Middle Types
9. 8:56Creating Equality Proofs
10. 9:44Transforming Equality Proofs
11. 13:32Challenge: Extensional Equality
12. 14:30Composing Functions
13. 15:51Goodies in the Paper