Page 1

Peek and Poke with Dependent Types

Page 2

House Today (1)

Uses GHC (the Glasgow Haskell Compiler)

Page 3

House Today (2)

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

Another Experiment: An Alfa version of House?

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

Alfa proofs (or lack thereof)

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

[5] Xavier Leroy: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, POPL 2006.