@Article{kavanagh_pientka_2024:_messag_obser_session,
  author =       {Kavanagh, Ryan and Pientka, Brigitte},
  title =        {Message-Observing Sessions},
  volume =       8,
  number =       {OOPSLA1},
  doi =          {10.1145/3649859},
  _checked =     {2024-10-24},
  _source =      {ev},
  abstract =     {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.},
  date =         {2024-04},
  eid =          142,
  journaltitle = {Proceedings of the ACM on Programming Languages},
  pagetotal =    29,
}