We introduce FuSes , a Fu nctional programming language that integrates Ses sion-typed concurrent process calculus code. A functional layer sits on top of a session-typed process layer. To generate and reason about open session-typed processes, the functional layer uses the contextual box modality extended with linear channel contexts. Due to the fundamental differences between the operational semantics of the functional layer and the concurrent semantics of processes, we bridge the two layers using a set of primitives to run and observe the behavior of closed processes within the functional layer. In addition, FuSes supports code analysis and manipulation of open session-typed process code. To showcase its benefit to programmers, we implement well-known optimizations, such as batch optimizations, as type-safe metaprograms over concurrent processes. Our technical contributions include a type system for FuSes , an operational semantics, a proof of its type safety, and an implementation.

We present Most, a process language with message-observing session types. Message-observing session types extend binary session types with type-level computation to specify communication protocols that vary based on messages observed on other channels. Hence, Most allows us to express global invariants about processes, rather than just local invariants, in a bottom-up, compositional way. We give Most a semantic foundation using traces with binding, a semantic approach for compositionally reasoning about traces in the presence of name generation. We use this semantics to prove type soundness and compositionality for Most processes. We see this as a significant step towards capturing message-dependencies and providing more precise guarantees about processes.

Session types employ a linear type system that ensures that communication channels cannot be implicitly copied or discarded. As a result, many mechanizations of these systems require modeling channel contexts and carefully ensuring that they treat channels linearly. We demonstrate a technique that localizes linearity conditions as additional predicates embedded within type judgments, which allows us to use structural typing contexts instead of linear ones. This technique is especially relevant when leveraging (weak) higher-order abstract syntax to handle channel mobility and the intricate binding structures that arise in session-typed systems. Following this approach, we mechanize a session-typed system based on classical linear logic and its type preservation proof in the proof assistant Beluga, which uses the logical framework LF as its encoding language. We also prove adequacy for our encoding. This shows the tractability and effectiveness of our approach in modelling substructural systems such as session-typed languages.

Polarized SILL is a programming language that combines functional programming with session-typed message-passing concurrency. It features general recursion; code and channel transmission; and synchronous and asynchronous communication. To reason about Polarized SILL programs, we develop the first program equivalence framework based on observable communications. We give meaning to Polarized SILL programs using an observed communication semantics (OCS). Our OCS is the first to support general recursion and code transmission. We then develop a communication-based testing equivalences framework and show that one of the equivalences captured by our framework coincides with barbed congruence, the canonical notion of process equivalence. Polarized SILL's operational semantics is specified using a multiset rewriting system. We introduce fairness for multiset rewriting systems to ensure that our OCS is well-defined in the presence of non-terminating processes, and use fairness properties to simplify reasoning about processes. This work lays the foundation for observational reasoning for session-typed languages with general recursion.

Parametrized fixed points are of particular interest to denotational semantics and are often given by “dagger operations” [Stephen L. Bloom and Zoltán Ésik, Fixed-Point Operations on ccc's. Part I, Theoretical Computer Science (ISSN 0304-3975) 155 (1996), 1–38, https://doi.org/10.1016/0304-3975(95)00010-0; Stephen L. Bloom and Zoltán Ésik, Iteration Theories. The Equational Logic of Iterative Processes, in: EATCS Monographs on Theoretical Computer Science, Springer-Verlag Berlin Heidelberg, ISBN 978-3-642-78034-9, 1993, xv+630 pp., https://doi.org/10.1007/978-3-642-78034-9; Stephen L. Bloom and Zoltán Ésik, Some Equational Laws of Initiality in 2CCC's, International Journal of Foundations of Computer Science 6 (1995) 95–118, https://doi.org/10.1142/S0129054195000081.]. Dagger operations that satisfy the Conway identities [Stephen L. Bloom and Zoltán Ésik, Fixed-Point Operations on ccc's. Part I, Theoretical Computer Science (ISSN 0304-3975) 155 (1996), 1–38, doi: https://doi.org/10.1016/0304-3975(95)00010-0.] are particularly useful, because these identities imply a large class of identities used in semantic reasoning. We generalize existing techniques to define dagger operations on ω-categories and on O-categories. These operations enjoy a 2-categorical structure that implies the Conway identities. We illustrate these operators by considering applications to the semantics of session-typed languages.

The SPARC TSO weak memory model is defined axiomatically, with a non-compositional formulation that makes modular reasoning about programs difficult. Our denotational approach uses pomsets to provide a compositional semantics capturing exactly the behaviours permitted by SPARC TSO. It uses buffered states and an inductive definition of execution to assign an input-output meaning to pomsets. We show that our denotational account is sound and complete relative to the axiomatic account, that is, that it captures exactly the behaviours permitted by the axiomatic account. Our compositional approach facilitates the study of SPARC TSO and supports modular analysis of program behaviour.