[e-lang] [Fwd: Re: E-on-Haskell]

[Mark S. Miller]

Forwarded with permission.

-------- Original Message --------
Subject: Re: [e-lang] E-on-Haskell
Date: Wed, 28 Jun 2006 18:00:52 -0700 (PDT)
From: oleg at pobox.com

[...]

	The Mint example, fully elaborated, can be found at

	http://pobox.com/~oleg/ftp/Haskell/mint.hs

Please feel free to distribute as you wish.

Speaking of references, I'd like to point out two. First, our paper
(which proves that references are expressible with delimited
continuations -- including the type setting) is available online:

	http://lambda-the-ultimate.org/node/1584

It has been accepted for ICFP. As you can see, I mention capabilities
in one of the messages posted on that thread.

Mainly, I'd like to strongly recommend the following paper

	http://www.cse.unsw.edu.au/~chak/papers/DEKC+06.html

which describes the working prototype of a seL4 (secure L4-like)
micro-kernel, which is written in Haskell, works with the system
emulator, runs the applications. In addition, it is converted into a
formal specification into Isabelle/HOL.

Incidentally, the design of seL4 is capability-based. Alas, the paper
doesn't explain that aspect -- it's the paper about Haskell rather
than microkernel. But you can see the datatype of capabilities, etc.

	Cheers,
	Oleg