Focusing on Refinement Typing (TOPLAS)

on YouTube ↗19m

" summary

A logically principled system that combines value-determined indices, focalized call-by-push-value, bidirectional typing and polarized subtyping generates SMT constraints for refinement types without leaving unsolvable existential unification variables; the algorithm solves all evars by the end of focusing stages, is decidable, and is proved sound and complete. Declarative typing is given a denotational CBPV semantics, yielding type soundness, logical consistency and total correctness (including pattern cover); examples show it synthesizes concrete sum and length indices for lists.

AI-written summary · about

" chapters (12)

1. 0:00Introduction to refinement typing
2. 0:46Manual refinements to measures
3. 2:32Challenges with fancy types
4. 3:59Append function with indices
5. 4:41Filter function with refinements
6. 6:28Refinement type grammar
7. 8:31Index solving system
8. 10:18Denotational semantics
9. 12:25Logical consistency
10. 13:08Empirical evidence FLUX
11. 13:30Summary and future
12. 14:35Q&A