University of Cambridge > Talks.cam > Microsoft Research Cambridge, public talks > Manifest Sharing with Session Types

Manifest Sharing with Session Types

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

Please note, this event may be recorded. Microsoft will own the copyright of any recording and reserves the right to distribute it as required.

Session-typed languages building on the Curry-Howard isomorphism between linear logic and session-typed communication guarantee session fidelity and deadlock freedom. Unfortunately, these strong guarantees exclude many naturally occurring programming patterns pertaining to shared resources. In this talk, I report on our work on manifest sharing, which introduces sharing into a session-typed language such that types are stratified into linear and shared layers with modal operators connecting the layers. The resulting language retains session fidelity but not the absence of deadlocks, which can arise from contention for shared processes. Our language can accommodate examples, such as producer-consumer queues and dining philosophers, that could previously not be expressed with linear session types alone, including a translation of the untyped asynchronous pi-calculus into our language.

This talk is part of the Microsoft Research Cambridge, public talks series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2019 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity