To: seminaire@pauillac.inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 27/06/06 - Paris - FR

           Vous pouvez vous abonner à nos annonces de séminaires
             http://pauillac.inria.fr/seminaires/subscribe.html

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
                         Amphi Turing du bâtiment 1

                            Mardi 27 juin, 10h30

                               -------------
                               George Necula
                               -------------

                     University of California, Berkeley

          =======================================================
          Using Dependent Types for Low-Level Systems Programming
          =======================================================

Types are recognized as a convenient specification mechanism, but simple types
are not expressive enough to describe relationships between values, as
necessary for low-level programming.  For example, in low-level code using
pointer arithmetic we must relate the value of the pointer with the variables
that store the bounds of the enclosing array.  We propose Deputy, a
lightweight specification mechanism based on dependent types for the C
programming language.  The novel features over previous uses of dependent
types is a mechanism for using them soundly in presence of pointers and
mutation, along with a technique for inference of dependencies for local
variables.  We show that dependent types are a natural specification mechanism
for enforcing common safe programming practices in existing C programs.
Finally, we describe our experience using this mechanism to efficiently
enforce memory safety for several Linux device drivers.