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