二元会话类型系统中演进特性研究  

A study on progress property in a type system for binary sessions

作　　者：钟发荣[1] 杨振国[1] 

机构地区：[1]浙江师范大学数理与信息工程学院,浙江金华321004

出　　处：《浙江师范大学学报（自然科学版）》2013年第2期127-132,共6页Journal of Zhejiang Normal University:Natural Sciences

基　　金：国家自然科学基金资助项目(60873234);浙江省计算机软件与理论重中之重学科开放基金资助项目(ZSDZZZZXK24)

摘　　要：提出了一个保持演进特性的二元同步会话类型系统,分析了进程通信中可能发生的死锁情形;同时结合会话类型的子类型概念和松弛对偶关系,定义了类型一致性等法则,确保了类型系统中进程通信一旦发生,合式进程在通道上不会发生死锁的情形.此外,还定义了递归会话类型的子类型和松弛对偶关系,提高了类型系统的灵活性.A type system with progress property for synchronous binary sessions was presented,and the cases that could lead to deadlocks were analyzed by examples.Moreover,type compliance was defined associating the subtype with relaxed duality relation for ensuring well-formed processes,that implied deadlock could be avoid when a communication begin in the present type system.In addition,the subtype and relaxed duality relation for both recursive and non-recursive session types were defined which improved the flexibility of the type system.

关 键 词：会话类型 PI-演算 子类型指派 演进特性 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]