Correctness of the Type System
Deadlock-freedom:(the case of an output obligation)
? + x:[?]/Oot; ?¨§ P
Every usage in ? + x:[?]/Oot is reliable
?+ is a strict partial order
P will eventually perform output on x (unless ¡Æinfinite loop¡Ç)
Previous slide
Next slide
Back to first slide
View graphic version