Higher-order processes, functions, and sessions: A monadic integration

Bernardo Toninho, Luis Caires, Frank Pfenning

Research output: Chapter in Book/Report/Conference proceedingConference contribution

43 Citations (Scopus)

Abstract

In prior research we have developed a Curry-Howard interpretation of linear sequent calculus as session-typed processes. In this paper we uniformly integrate this computational interpretation in a functional language via a linear contextual monad that isolates session-based concurrency. Monadic values are open process expressions and are first class objects in the language, thus providing a logical foundation for higher-order session typed processes. We illustrate how the combined use of the monad and recursive types allows us to cleanly write a rich variety of concurrent programs, including higher-order programs that communicate processes. We show the standard metatheoretic result of type preservation, as well as a global progress theorem, which to the best of our knowledge, is new in the higher-order session typed setting.

Original languageEnglish
Title of host publicationProgramming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Proceedings
Pages350-369
Number of pages20
Volume7792 LNCS
DOIs
Publication statusPublished - 2013
Event22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013 - Rome, Italy
Duration: 16 Mar 201324 Mar 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7792 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Conference

Conference22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013
CountryItaly
CityRome
Period16/03/1324/03/13

Fingerprint Dive into the research topics of 'Higher-order processes, functions, and sessions: A monadic integration'. Together they form a unique fingerprint.

Cite this