2020/02/05 by Ryan Kavanagh, Kavanagh, Ryan
Computer Science · #Distributed systems and fault tolerance #F.3.2 #FOS: Computer and information sciences #Formal Methods in Verification #Logic, programming, and type systems #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.2002.01960
openalex publication_date 2020/02/05 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.