Dependent types for low-level programming

Jeremy Condit, Matthew Harren, Zachary Anderson, David Gay, George C. Necula
[ISBN] [Google Scholar] [DBLP] [Citeseer]
Read: 14 June 2021

Programming Languages and Systems
Springer Berlin Heidelberg
Berlin, Heidelberg
Pages 520-535
Note(s): dependent type, Cyclone language
Papers: furr:pldi:2005

Deputy is a dependent type system for C that allows programmers to annotate pointers and tagged unions, infers annotations, and mostly performs compile-time checks that array/pointer offsets are in bounds but (to preserve decidability) falls back to run-time checks when necessary.

The type system is flow-insensitive (contrast with furr:pldi:2005) and the assignment rule is related to Hoare logic. Unlike CCured and the Cyclone language, Deputy does not need fat pointers.

The evaluation looked at 3 SPEC benchmarks, 9 Olden benchmarks, ptrdist benchmarks, and TinyOS benchmarks and looked at the number of lines changed (around 2-4% on average and up to 11%) and the runtime overhead (less than 25% in half the tests but up to 100%).