EVENT

Talk by Prof. Nobuko Yoshida: "On Polymorphic Sessions and Functions (ESOP 2018)"

It is our pleasure to announce that Prof. Nobuko Yoshida from Imperial College London will give a talk on polymorphic sessions and functions; see below for the details. All are welcome!

Date:

July 24 (Tue.)

Time:

16:00-17:00

Place:

National Institute of Informatics
Room 1208, 12th floor

Abstract:

I first talk about the origin of session types and a summary of the activities in our session types group in Imperial. The rest of the talk also aims to non-specialists so everybody is welcome.

This work exploits the logical foundation of session types to determine what kind of type discipline for the π-calculus can exactly capture, and is captured by, λ-calculus behaviours. Leveraging the proof theoretic content of the soundness and completeness of sequent calculus and natural deduction presentations of linear logic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processes encodings between a polymorphic session π-calculus and a linear formulation of System F. We are then able to derive results of the session calculus from the theory of the λ-calculus: (1) we obtain a characterisation of inductive and coinductive session types via their algebraic representations in System F; and (2) we extend our results to account for value and process passing, entailing strong normalisation.

Contact:

Josh Ko ( hsiang-shang [at] nii.ac.jp )