Dependent Types for Low-Level Programming
Jeremy Paul Condit and Matthew Thomas Harren and Zachary Ryan Anderson and David Gay and George Necula
EECS Department, University of California, Berkeley
Technical Report No. UCB/EECS-2006-129
October 13, 2006
http://www2.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-129.pdf
We describe the key principles of a flexible dependent type system for low-level imperative languages. Two major contributions are (1) a new typing rule for handling mutation that follows the model of Hoare's axiom for assignment and (2) a technique for automatically inferring dependent types for local variables. This type system is more expressive than previous dependent type systems because types can now depend on mutable variables; in addition, it improves ease of use by inferring dependent type annotations for local variables. Decidability is addressed by emitting run-time checks for those conditions that cannot be checked statically.
Using these principles, we have designed Deputy, a dependent type system for C whose types allow the programmer to describe several common idioms for the safe use of pointers and tagged unions. We have used Deputy to enforce memory safety properties in a number of common benchmark suites as well as in Linux device drivers and TinyOS components. These experiments show that Deputy's dependent types are useful in a wide range of C programs and that they have a relatively low annotation burden and performance cost.
BibTeX citation:
@techreport{Condit:EECS-2006-129, Author= {Condit, Jeremy Paul and Harren, Matthew Thomas and Anderson, Zachary Ryan and Gay, David and Necula, George}, Title= {Dependent Types for Low-Level Programming}, Year= {2006}, Month= {Oct}, Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-129.html}, Number= {UCB/EECS-2006-129}, Abstract= {We describe the key principles of a flexible dependent type system for low-level imperative languages. Two major contributions are (1) a new typing rule for handling mutation that follows the model of Hoare's axiom for assignment and (2) a technique for automatically inferring dependent types for local variables. This type system is more expressive than previous dependent type systems because types can now depend on mutable variables; in addition, it improves ease of use by inferring dependent type annotations for local variables. Decidability is addressed by emitting run-time checks for those conditions that cannot be checked statically. Using these principles, we have designed Deputy, a dependent type system for C whose types allow the programmer to describe several common idioms for the safe use of pointers and tagged unions. We have used Deputy to enforce memory safety properties in a number of common benchmark suites as well as in Linux device drivers and TinyOS components. These experiments show that Deputy's dependent types are useful in a wide range of C programs and that they have a relatively low annotation burden and performance cost.}, }
EndNote citation:
%0 Report %A Condit, Jeremy Paul %A Harren, Matthew Thomas %A Anderson, Zachary Ryan %A Gay, David %A Necula, George %T Dependent Types for Low-Level Programming %I EECS Department, University of California, Berkeley %D 2006 %8 October 13 %@ UCB/EECS-2006-129 %U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-129.html %F Condit:EECS-2006-129