This paper is in the area of theory related to concurrency and threading. It is about reasoning noninterference properties in a concurrent programming language with information flow type systems. The work uses the proof assistant Isabelle/HOL to check the noninterference properties. It addresses more general language constructs than earlier works.

Section 1 introduces the noninterference property, and its relation to the security of programs. It describes the problems posed by concurrency in this context, and cites various solutions. After a brief section on Isabelle/HOL, section 3 presents the work formally. The language under consideration is defined. The relevant properties of type systems and operational semantics are presented. The language is an extension of the While language, with parallel and scheduling operators. Section 4 describes theories of the noninterference property of scheduling programs. The fifth section claims that the work demonstrates the use of proof assistance in the verification of type systems of programming languages.

The paper presents useful work in the area of security of concurrent programs. Theories are presented precisely. However, the paper does not provide examples or explanations for the theories, which may make it difficult for nontheoreticians to understand. With respect to machine checking, no experimental setup is described. The work is definitely inspirational for researchers using proof assistants in designing programming languages.