A functional approach to memory-safe operating systems (2011) [pdf]

As you’d expect, this involves creating a monad for all the actual messy OS stuff. The capabilities therein are described by quite nice type classes (potentially representing hardware capabilities or your own address space, for example), which is interesting because you could build something like OpenBSD’s pledge that’s formally provable at the type level etc. I remember another somewhat functional approach to OS programming being to hide the privileged bits of system calls behind curried functions so your process gets effectively a private view of the kernel:

http://4e.iwp9.org/papers/usecsys.pdf

All very much over my head, of course, but always interesting to see paradigms prove robust all the way up and down the software stack.

This should have an (2011) in the title.

luu, could you say a few words on what you found interesting about this thesis? The first chapter sounds impressive, but later it only seems to be defining a monad around typical operating system tasks. That means you still have to deal with GC, and I would not call that approach "well integrated with purely functional programming", as it essentially defines an imperative DSL. But I have only looked at this briefly and I would appreciate deeper insight.

Related efforts:

https://www.microsoft.com/en-us/research/project/singularity...

https://en.wikipedia.org/wiki/Midori_(operating_system)

http://jnode.ro/

None are functional but as noted in other comments, you end up needing to do everything in a monad anyway if you try to do an OS in an FP language. An OS is all about managing a large and fundamentally imperative block of hardware state so pure FP isn't an obvious fit.