A Logical Analysis
•
Types satisfy precisely the laws of the modal
logic S4
•
Multiple world semantics as computation stages
•
Admits several concrete realizations