Manifest Sharing with Session Types

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

• Stephanie Balzer, Carnegie Mellon University
• Friday 08 September 2017, 11:00-12:00
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.