Title: "Operating Systems in Haskell: Implementations and Models"

Author : Andrew Tolmach (Gallium Inria - DCS Portland State University)

Abstract:
I'll describe an approach to building and verifying operating systems
written in the functional language Haskell.  The approach is based on
a monadic interface to low-level hardware features, which 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.  I'll 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.

I will also discuss initial approaches to proving useful properties of
these kernels, such as separation between user processes.  Some of
these approaches rely on modeling the behavior of the hardware
interface inside (pure) Haskell, and I will describe the structure of
our model.

(This is joint work with other members of the Programatica team at
Portland State University.)