Discussion: Session Types as Intuitionistic Linear Propositions
Read the paper Session Types as Intuitionistic Linear Propositions.
Before class, add comments or questions here.
How does it really work in Tcut and Tcut! rules?(top of page 5)
What's the main different between this two?
What exactly is (νy)P (name restriction)?
What are pi-calculi and what are they used for?
Is there an implementation(compiler?) of the type system presented in this paper that could be used for modeling or verifying particular concurrent systems?