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. © 2013 Springer-Verlag.
CITATION STYLE
Toninho, B., Caires, L., & Pfenning, F. (2013). Higher-order processes, functions, and sessions: A monadic integration. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7792 LNCS, pp. 350–369). https://doi.org/10.1007/978-3-642-37036-6_20
Mendeley helps you to discover research relevant for your work.