skip to main content
Department of Computer Science University of Colorado Boulder
cu: home | engineering | mycuinfo | about | cu a-z | search cu | contact cu cs: about | calendar | directory | catalog | schedules | mobile | contact cs
home · events · colloquia · 2006-2007 · 

Colloquium - Condit


Deputy: Dependent Types for Safe Systems Software
University of California, Berkeley
Jeremy Condit photo

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 PhD 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 AB summa cum laude from Harvard University, and he received his MS 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.

Hosted by Amer Diwan.

The Department holds colloquia throughout the Fall and Spring semesters. These colloquia, open to the public, are typically held on Thursday afternoons, but sometimes occur at other times as well. If you would like to receive email notification of upcoming colloquia, subscribe to our Colloquia Mailing List. If you would like to schedule a colloquium, see Colloquium Scheduling.

Sign language interpreters are available upon request. Please contact Stephanie Morris at least five days prior to the colloquium.

See also:
Department of Computer Science
College of Engineering and Applied Science
University of Colorado Boulder
Boulder, CO 80309-0430 USA
Send email to

Engineering Center Office Tower
ECOT 717
FAX +1-303-492-2844
XHTML 1.0/CSS2 ©2012 Regents of the University of Colorado
Privacy · Legal · Trademarks
May 5, 2012 (13:29)