Linearity, Control Effects, and Behavioral Types

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

19 Citations (Scopus)

Abstract

Mainstream programming idioms intensively rely on state mutation, sharing, and concurrency. Designing type systems for handling and disciplining such idioms is challenging, due to long known conflicts between internal non-determinism, linearity, and control effects such as exceptions. In this paper, we present the first type system that accommodates non-deterministic and abortable behaviors in the setting of session-based concurrent programs. Remarkably, our type system builds on a Curry-Howard correspondence with (classical) linear logic conservatively extended with two dual modalities capturing an additive (co)monad, and provides a first example of a Curry-Howard interpretation of a realistic programming language with built-in internal non-determinism. Thanks to its deep logical foundations, our system elegantly addresses several well-known tensions between control, linearity, and non-determinism: globally, it enforces progress and fidelity; locally, it allows the specification of non-deterministic and abortable computations. The expressivity of our system is illustrated by several examples, including a typed encoding of a higher-order functional language with threads, session channels, non-determinism, and exceptions.
Original languageEnglish
Title of host publicationProgramming Languages and Systems
EditorsH. Yang
PublisherSpringer
Pages229-259
Number of pages31
DOIs
Publication statusPublished - 2017
Event26th European Symposium on Programming (ESOP 2017), Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2017, Uppsala, Sweden, April 22-29, 2017. -
Duration: 22-Apr-201729-Apr-2017

Publication series

Name Lecture Notes in Computer Science
PublisherSpringer
Volume10201

Conference

Conference26th European Symposium on Programming (ESOP 2017), Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2017, Uppsala, Sweden, April 22-29, 2017.
Period22/04/201729/04/2017

Cite this