To: seminaire@pauillac.inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Cristal - 24/03/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

                          Vendredi 24 mars, 10h30

                               --------------
                               Andrew Tolmach
                               --------------

                         Portland State University

     =================================================================
     A Principled Approach to Operating System Construction in Haskell
     =================================================================

We describe a monadic interface to low-level hardware features that is a
suitable basis for building operating systems in Haskell. The interface
includes primitives for controlling memory management hardware, user-mode
process execution, and low-level device I/O. The interface enforces memory
safety in nearly all circumstances. Its behavior is specified in part by
formal assertions written in a programming logic called P-Logic. The interface
has been implemented on bare IA32 hardware using the Glasgow Haskell Compiler
(GHC) runtime system.  We show how a variety of simple O/S kernels can be
constructed on top of the interface, and will demonstrate a simple OS in which
the kernel, window system, and all device drivers are written in Haskell. We
will also discuss various approaches to proving properties of these kernels.