Types provide a convenient and accesible mechanism for specifying program invariants. Dependent types extends simple types with the ability to express invariants relating multiple state elements. While such dependencies likely exists in all programs, they play a fundamental role in low-level programming. These dependencies are essential even to prove simple properties like memory safety. In this talk I will present an overview of a type system that combines dependent types and mutation for variables and for heap-allocated structures, and a technique for automatically inferring dependent types.

Note: The talk will be based on the paper Dependent Types for Low-Level Programming by Jeremy Condit, Mathew Harren, Zachary Anderson, David Gay, and George Necula.