Page 1

Dependability through Dependent Types

(or Peek and Poke with Dependent Types)

Thomas Hallgren

SICS, 2008-10-21

(based on a ProgLog meeting talk, Chalmers, December 2006)

Page 2

How safe is House?

Uses GHC (the Glasgow Haskell Compiler)

Page 3
How safe is House?

Does the Haskell type system give us what we need?

Page 4

At the Machine Level...

Primitives for memory access

Page 5

Safety Through Abstraction

Page 6

Hardware Monad Examples

Page 7

SafeHouse: an experiment

Page 8

A Minimal Compiler and Run-Time System

Page 9

Compiler and run-time system

Based on the <ν,G> machine [2]

Page 10

An example

Hello world!

Page 11

Peek and Poke again

Primitives for memory access

Page 12

Abstraction for limited memory access

Page 13

Text screen buffer access (1)

Page 14

Text screen buffer access (2)

Using Predicate Based Subtyping

Page 15

Abstraction for displaying text

Page 16


Page 17

Example of extended static checking

Displaying strings that fit on the screen

Page 18

Hello world!

Page 19


Page 20

Future work?

Page 21

The End

Any more questions?

Page 22


Page 23