ezyang’s blog

the arc of software bends towards understanding

Session types, subtyping and dependent types

While I was studying session type encodings, I noticed something interesting: the fact that session types, in their desire to capture protocol control flow, find themselves implementing something strongly reminiscent of dependent types. Any reasonable session type encoding requires the ability to denote choice: in Simon Gay’s paper this is the T-Case rule, in Neubauer […]

  • September 17, 2010