paper on typing for non-interference of concurrent threads

We would like to announce the availability of the following paper.


  Non-interference for concurrent programs and thread systems

  Gérard Boudol and Ilaria Castellani

We propose a type system to ensure the property of noninterference in a
system of concurrent programs, described in a standard imperative
language enriched with parallelism. Our proposal is in the line of some
recent work by Irvine, Volpano and Smith. Our type
system seems more natural and less restrictive than that originally
presented by these authors, for the concurrent case. Moreover,
we show how to extend the language in order to formalise scheduling
policies for systems of sequential threads. The type system is
extended to the new constructs, and we show that noninterference still
holds, while remaining in a nonprobabilistic setting. 


Note: although this paper builds on our ICALP'2001 paper, it uses a
slightly different type system for concurrent programs without     
scheduling, and presents a more general solution for scheduling
sequential threads. 

The paper is available from our web pages:



Comments are welcome!