Sciweavers

CSFW
1997
IEEE

Eliminating Covert Flows with Minimum Typings

13 years 7 months ago
Eliminating Covert Flows with Minimum Typings
A type system is given that eliminates two kinds of covert flows in an imperative programming language. The first kind arises from nontermination and the other from partial operations that can raise exceptions. The key idea is to limit the source of nontermination in the language to constructs with minimum typings, and to evaluate partial operations within expressions of try commands which also have minimum typings. A mutual progress theorem is proved that basically states that no two executions of a well-typed program can be distinguished on the basis of nontermination versus abnormal termination due to a partial operation. The proof uses a new style of programming language semantics which we call a natural transition semantics.
Dennis M. Volpano, Geoffrey Smith
Added 05 Aug 2010
Updated 05 Aug 2010
Type Conference
Year 1997
Where CSFW
Authors Dennis M. Volpano, Geoffrey Smith
Comments (0)