Correctness of the Type System
No immediate deadlock:Well-typed processes are not in deadlock
+
Subject reduction:Well-typedness is preserved by reduction
?
Deadlock-freedom:Well-typed processes never fall into deadlock throughout reduction
Previous slide
Next slide
Back to first slide
View graphic version