FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
A New Linear Logic for Deadlock-Free Session-Typed Processes (Talk Abstract)

Authors: Ornela Dardha and Simon J. Gay

Paper Information

Title:A New Linear Logic for Deadlock-Free Session-Typed Processes (Talk Abstract)
Authors:Ornela Dardha and Simon J. Gay
Proceedings:WiL Short Papers and Abstracts
Editors: Valeria de Paiva, Amy Felty and Ursula Martin
Keywords:classical linear logic, pi-caclulus, session types, Curry-Howard correspondence, deadlock-freedom, priorities
Abstract:

ABSTRACT. We propose a new type system for deadlock-free session-typed π-calculus, a core concurrent programming language, by integrating for the first time, two separate lines of work. The first is the propositions-as-types approach by Caires and Pfenning, which provides a linear logic foundation for session types and guarantees deadlock-freedom. The second is Kobayashi’s approach in which types are annotated with priorities for detecting cyclic dependencies between communication operations. The outcome is a new and more expressive variant of classical linear logic with a proof assignment that gives a session type system with Kobayashi-style priorities.

Pages:1
Talk:Jul 08 10:15 (Session 34N)
Paper: