并发语言OCCAM的指称语义

在研究关于 CSP并发指称语义的不同研究方法的基础之上 ,利用广义状态的概念和完备距离空间作为指称的方法 ,讨论了 OCCAM的一个子集 OCCAM/ TOY的并发语义。针对目前交叠并发语义研究方法的问题和不足 ,首先在 OCCAM/ TOY的语法中引入了一类具体的原子语句 ,并从语义上考虑了原子语句的语义对整个程序语义的影响 ;其次 ,对于通常语义方法中合并处理的一对通信原语的一次通信分开处理 ,描述了单个通信步骤的语义及其对程序的影响。在构造语义域时 ,利用完备距离空间作为指称 ,讨论了在距离空间范畴中语义域议程的解的存在性 ;并且在定义语义函数时 ,保证了递归定义的语义函数的存在性。给出了 OCCAM/ TOY的完全意义上的并发指称语义 ,既体现了由于并发而导致的执行过程的不确定性 。

对象的行为表示及其应用

主要讨论了一种描述对象活动的方法 ,提出了活动体的概念 ,并给出了它的三元组形式 活动体是对象式系统中具有通信能力的最小单位 ,由此可以构造对象乃至系统的交互 (通信 )行为

A Syntactic Proofof the Conservativity of λ_ω over λ_2

In this paper, the relationship between the second order typed - calculus 2 and its higher order version is discussed . A purely syntactic proof of the conservativity of over 2 is given.