The Programatica project and Galois have each had several years of experience in the development and analysis of high-assurance systems software using functional programming, specifically the Haskell programming language.
Programatica developed both applications and reasoning tools for Haskell, including:
a prototype operating system that boots and runs on bare metal
(IA32) and in which the kernel, a small collection of device drivers, and
several sample applications, have all been implemented in Haskell. The
House kernel supports protected execution of arbitrary user-level binaries
and manages the virtual memory of each such process by direct manipulation of the page table data structures that are used by the hardware
- Osker, a prototype separation kernel coded in Haskell. Several variants
have been built, including both high-level models and simple executables.
(For details about House and Osker, see Hallgren, Jones, Leslie and Tolmach: "A Principled Approach to Operating System Construction in Haskell".)
- A formal semantics for Haskell (including its core type system, its module
system, and its dynamic semantics) that is precise enough to support
- P-Logic, a programming logic specifically designed to be faithful to Haskell's
lazy evaluation semantics, and Plover, a dedicated prover for P-Logic assertions.
- Tools for embedding the GHC Core Haskell language into the HOLCF
logic of the Isabelle theorem prover. This work relies on an encoding of
(parts of) the formal semantics as Isabelle theory files and allows us to
state and reason about the behavior of Haskell programs. (For more information, see Brian Huffman's presentations.)
- Hobbit, a prototype programming language that combines higher-order functional programming with bit-level data.
Galois has also developed a number of Haskell applications and tools, including but not limited to:
back to main page
- The Trusted Services Engine (TSE) is a highly scalable cross-domain web
server and file store that lets users with differing security clearances
share file-based information securely across multiple networks and domains.
- The Haskell Program Coverage (HPC) toolkit allows a programmer to
identify the code exercised by a test suite.