[Haskell] Haskell / Full-fledge verified OS

[William DUCK]

Hello Misters,

As you are iin functional programming, I am 
asking your help.

I am attempting to build up a team.

I believe it's time for a full-fledge verified OS.

http://www.ertos.nicta.com.au/publications/papers/Tuch_KH_05.pdf

Here are my guidelines :

http://www.cse.ogi.edu/~hallgren/House/

*OS-design :

http://www.ertos.nicta.com.au/publications/papers/Leslie_06.pdf ( for 
transition )

http://www.marcus-brinkmann.org/hurd-ng.pdf

http://www.eecg.toronto.edu/~tornado/ ( scalability / hot swapping )

*kernel :

http://os.inf.tu-dresden.de/L4/L4.Sec/

http://www.doclsf.de/papers/vstte06.pdf#search=%22formalising%20high%20performance%20kernel%22

*network stack :

http://www.cl.cam.ac.uk/~pes20/Netsem/

*programming :

http://fling-l.seas.upenn.edu/~plclub/cgi-bin/poplmark/index.php?title=The_POPLmark_Challenge

http://www.informatik.uni-bonn.de/~loeh/GFP.html

http://maude.cs.uiuc.edu/tools/scc/

*proving environment :

http://isabelle.in.tum.de/

http://www.cl.cam.ac.uk/Research/HVG/HOL/

*compiler :

http://pauillac.inria.fr/~xleroy/compcert-backend/

http://www.score.is.tsukuba.ac.jp/~okuma/vc/

Any suggestions ?

Thank you for your answer,

If you want to contact me, my mail is guillaume_dot_fortaine_at_wanadoo_dot_fr

I will set up a mailing-list, a web server, a wiki and an IRC

Best Regards,


Best Regards,

                          Guillaume FORTAINE