A Domain Semantics for Higher-Order Recursive Processes
Ryan Kavanagh
A Domain Semantics for Higher-Order Recursive Processes
May 10, 2020
72
2002.01960v3 [cs.PL]
The polarized SILL programming language uniformly integrates
functional programming and session-typed message-passing
concurrency. It supports general recursion, asynchronous and
synchronous communication, and higher-order programs that
communicate channels and processes. We give polarized SILL a
domain-theoretic semantics—the first denotational semantics for a
language with this combination of features. Session types in
polarized SILL denote pairs of domains of unidirectional
communications. Processes denote continuous functions between these
domains, and process composition is interpreted by a trace
operator. We illustrate our semantics by validating expected
program equivalences.