@Thesis{kavanagh_2021:_commun_based_seman,
  abstract =	 {Communicating systems are ubiquitous, but they are
		  hard to get right. Fortunately, we can use
		  session-typed programming languages to help us
		  correctly implement communicating systems.  \par In
		  this thesis, we present novel semantics and
		  reasoning techniques for Polarized SILL, a
		  higher-order session-typed programming
		  language. Polarized SILL coherently integrates
		  functional programming with asynchronous
		  message-passing concurrency. It also supports
		  recursive communication protocols, code
		  transmission, and synchronization.  \par Our
		  contributions are unified by their commitment to the
		  process abstraction: communication is the only
		  phenomenon of processes. As a result, our semantics
		  define the meaning of processes in terms of their
		  communications. Concretely, we give Polarized SILL
		  three communication- based semantics:
		  \begin{enumerate} \item An observed communication
		  semantics. It defines the meaning of processes to be
		  the communications we observe during their
		  executions. Ours is the first to support rich
		  protocols like recursion, code transmission, and
		  synchronization.  \item A communication-based
		  testing equivalences framework. It deems processes
		  to be equivalent whenever they are indistinguishable
		  through experimentation. One of our testing
		  equivalences coincides with barbed congruence, the
		  canonical notion of process equivalence.  \item A
		  denotational semantics. It defines the meaning of
		  communicating processes to be stable continuous
		  functions between dI-domains of session-typed
		  communications.  It adapts ideas from Kahn semantics
		  for dataflow networks to handle bidirectional
		  communications, and it is sound relative to barbed
		  congruence. Importantly, it lets us reason modularly
		  about programs.  \end{enumerate} \par We illustrate
		  our techniques by applying them to several case
		  studies.},
  author =	 {Kavanagh, Ryan},
  date =	 {2021-09-30},
  institution =	 {Computer Science Department, Carnegie Mellon
		  University},
  location =	 {Pittsburgh, Pennsylvania},
  pagetotal =	 {x+313~\ppno},
  title =	 {Communication-Based Semantics for Recursive Session
		  Typed Processes},
  type =	 {phdthesis},
}