This thesis presents Deputy, a dependent type framework that allows programmers to annotate existing C code with more refined types. In particular, dependent types allow programmers to relate multiple state elements, such as a pointer and its bounds, or a union and its tag. In doing so, we address several technical hurdles involved with dependent types. First, we address the issue of mutation in the presence of dependencies by using insights from axiomatic semantics. Second, we handle the problem of undecidability by using run-time checks where necessary. Third, we address usability challenges with a novel inference mechanism called automatic dependencies.

Once this framework is established, we show how it can be instantiated to support the dependent types required by modern systems code. In addition, we discuss several real-world applications of Deputy, including small and medium-size benchmarks as well as the Linux kernel itself. These benchmarks allow us to evaluate Deputy's annotation burden and performance in the context of real-world code.