file.pdf (303.94 kB)
Download file

Higher-Order Processes, Functions, and Sessions: A Monadic Integration

Download (303.94 kB)
journal contribution
posted on 01.01.1983, 00:00 by Bernardo Toninho, Luis Caires, Frank Pfenning

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.

History

Publisher Statement

All Rights Reserved

Date

01/01/1983

Usage metrics

Exports