论文标题
在会话键入，概率多项式时间和密码实验（长版）上
On Session Typing, Probabilistic Polynomial Time, and Cryptographic Experiments (Long Version)
论文作者
论文摘要
会话类型的系统被引入，该系统由咖喱霍华德对应关系应用于有限的线性逻辑，然后扩展了具有概率选择和接地类型的如此获得的类型系统。获得的系统满足了预期的属性，例如降低受试者和进度，但也是出乎意料的，例如在减少过程所需的时间上绑定了多项式。这使该系统适合于所谓的密码学计算模型进行建模实验和证明。
A system of session types is introduced as induced by a Curry Howard correspondence applied to Bounded Linear Logic, and then extending the thus obtained type system with probabilistic choices and ground types. The obtained system satisfies the expected properties, like subject reduction and progress, but also unexpected ones, like a polynomial bound on the time needed to reduce processes. This makes the system suitable for modelling experiments and proofs from the so-called computational model of cryptography.
