OPLSS 俄勒冈编程语言暑期学校

不懂编程语言, 也不懂数学和逻辑, 我该怎么办呢?

白鹤衔苦桃, 千里作一息. 欲往蓬莱山, 将此充粮食. 未达毛摧落, 离群心惨恻. 却归旧来巢, 妻子不相识.

随便记点笔记, 但是我不能保证这里的笔记的准确性.

会话类型并发编程

• 演员模型 (actor model)
• 会话类型 (session types)
• 线性逻辑 (linear logic)

消息传递并发

通过沿信道交换消息进行计算的进程

• $n$-ary信道
• 非确定性
• 形式化基础: 进程演算, 例如$\pi$演算

消息传递队列

• 移动性 (mobility)
• 高阶信道 (higher-order channel)

消息交换协议的类型

会话类型 (Honda, Kohei. 1993. 'Types for Dyadic Interaction'. In CONCUR'93, edited by Eike Best, 715:509–523. Lecture Notes in Computer Science. Springer, Berlin, Heidelberg.)

A ::= ?[T].A'
   |  ![T].A'
   |  &{l_1: A_1; ...; l_n: A_n}  (external choice)
   |  ⊕{l_1: A_1; ...; l_n: A_n}  (internal choice)
   |  end
   |  X
   |  μX.A'
T ::= A
   |  basic types such as int, char, ...

queue = &{enq: ?[char].queue;
          deq: ⊕{none: end; some: ![char].queue}}

[client] ---(q: queue)--- [O]-[P]-[L]-[ ]

q: ... (queue)
  send 'enq' along q
q: ?[char].queue
  send 'S' along q
q: queue

观察: 信道/进程的类型随着消息的交换而改变

会话类型中的保持 (session fidelity)

guarantees that expectation of client matches with the one of providers if they do initially

线性逻辑

线性逻辑拒绝弱化规则和收缩规则, 这是因为在线性逻辑中命题相当于资源, 我们不能随意添加或删除. 弱化和丢弃资源有关, 收缩和复制资源有关.