Dependent session types via intuitionistic linear type theory
Dependent session types via intuitionistic linear type theory
复制标题
通过直觉线性类型理论的依赖会话类型
DOI：
10.1145/2003476.2003499
复制
发表时间：
2011
期刊：
影响因子：
5.2
通讯作者：
F. Pfenning
中科院分区：
文献类型：
--
作者：
Bernardo Toninho;Luís Caires;F. Pfenning
我们将线性类型理论解释为一项通过pi微积分扩展的相关会话类型。类型系统允许我们在会话上表达丰富的约束，例如接口契约和携带证明的认证，它们超越了现有的会话类型系统，并且在纯逻辑基础上得到了证明。我们可以使用证明无关性进一步改进我们的解释，以消除可信各方之间证明的通信开销。我们的技术成果包括类型保存和全局进展，在我们的设置中，这自然意味着遵循由依赖类型表示的接口契约中声明的所有属性。
We develop an interpretation of linear type theory as dependent session types for a term passing extension of the pi-calculus. The type system allows us to express rich constraints on sessions, such as interface contracts and proof-carrying certification, which go beyond existing session type systems, and are here justified on purely logical grounds. We can further refine our interpretation using proof irrelevance to eliminate communication overhead for proofs between trusted parties. Our technical results include type preservation and global progress, which in our setting naturally imply compliance to all properties declared in interface contracts expressed by dependent types.