[cap-talk] "A Contribution to Techniques for Building Dependable Software Systems"

[lists at notatla.org.uk]

> Interesting paper:
> http://www2.fiit.stuba.sk/~kosik/doc/ecbs-eerc-2011.pdf
> A Contribution to Techniques for Building Dependable Software Systems
> by Matej Kosic and Jiri Safarik

I'm sure I've missed understanding some details.

Does the whole of this small OS compile to a single program?
If not I don't see how compile-time type checking is done on
the capability interfaces between client and server components.

For instance as in Section VI if the callback capability
given by a client to a server (supposed to be used for upward
responses) is actually a regular capability not allowing
donating-send then at what point is it detected and what
happens?

The dc2 and p tarfiles contain a link to a file not provided:
  lrwxrwxrwx common.bib -> /home/kosik/doc/latex/common/common.bib