Relevance to current work

• Although designed to model hardware, the Chip Model can also be seen as a model of a simple operating system.
• Channel separation corresponds to separation between processes.
• The proof techniques outlined in this talk are likely to be applicable when proving separation properties for our microkernel implementation in Haskell.