Anzeige
Erschienen in:
2016 | OriginalPaper | Buchkapitel
Conflation Confers Concurrency
verfasst von : Robert Atkey, Sam Lindley, J. Garrett Morris
Erschienen in: A List of Successes That Can Change the World
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Abstract
Session types provide a static guarantee that concurrent programs respect communication protocols. Recent work has explored a correspondence between proof rules and cut reduction in linear logic and typing and evaluation of process calculi. This paper considers two approaches to extend logically-founded process calculi. First, we consider extensions of the process calculus to more closely resemble \(\pi \)-calculus. Second, inspired by denotational models of process calculi, we consider conflating dual types. Most interestingly, we observe that these approaches coincide: conflating the multiplicatives (\(\otimes \) and \(\invamp \)) allows processes to share multiple channels; conflating the additives (\(\oplus \) and \( {\, \& \,}\)) provides nondeterminism; and conflating the exponentials (\({!}\) and \({?}\)) yields access points, a rendezvous mechanism for initiating session typed communication. Access points are particularly expressive: for example, they are sufficient to encode concurrent state and general recursion.