Deputy: Dependent Types for Safe Systems Software

Dr. Condit is from the University of California, Berkeley
Programming language tools offer powerful mechanisms for improving the
safety and reliability of systems code. This talk presents Deputy, a
type system and compiler for enforcing type and memory safety in
real-world C programs such as Linux device drivers and the Linux
kernel itself. Deputy's type system uses dependent types, a language
mechanism that allows programmers to describe common C idioms in an
intuitive fashion.

The Deputy project offers contributions to both systems and
programming languages. From a systems perspective, Deputy is
attractive because it can provide fine-grained safety guarantees in a
modular and incremental fashion; for example, Deputy can be used to
enforce type and memory safety in Linux device drivers without
requiring changes to the kernel. The SafeDrive recovery system for
Linux device drivers uses Deputy for isolation and failure detection,
and as a result, it is both simpler and faster than previous systems
for isolating software extensions. From a language perspective,
Deputy shows how to reason about dependent types in imperative code.
Deputy has fewer restrictions on mutation than previous systems, and
it uses run-time checks and several inference techniques to ensure
decidability and usability.
Jeremy Condit is a graduate student who is currently completing his
Ph.D. at the University of California, Berkeley. His research
interests focus on using programming language tools and techniques to
address the challenges of building large software systems. He
received his A.B. summa cum laude from Harvard University, and he
received his M.S. from the University of California, Berkeley. He is
a recipient of the NSF Graduate Research Fellowship, and he received
the Best Paper Award at ETAPS 2005 from the European Association for
Programming Languages and Systems.