中国科学院计算机科学重点实验室

一、概况 计算机科学实验室依托于中科院软件所,始建于1993年,1994年12月经中科院批准对外开放.实验室有多位我国计算机软件科学事业的开拓者,曾获得国家自然科学奖一、二、三等奖、国家科技进步奖二等奖、全国科学大会重大成果奖及何梁何利科技进步奖等.     

面向传值进程的一阶模态逻辑的可判定性与模型检测

对于面向传值进程的Hennessy-Milner逻辑的一阶扩充HML(FO), 给出了基于带赋值的符号迁移图的语义解释. 证明了HML(FO)的子逻辑HML(FO²)是满足性可判定的, 并且讨论了判定的复杂性. 最后给出传值进程关于HML(FO²)的模型检测的可判定性结果.     

π-演算观察等价的推理系统

提出带递归π－演算观察等价的推理系统，并证明了在受卫递归有穷控制子集上的完备性。该系统由推理规则和等式公理两部分组成，其断言采用条件等式的形式，直接刻画了进程项之间的符号互模拟关系。     

中国科学院计算机科学重点实验室

一、概　况　　计算机科学实验室依托于中科院软件所 ,始建于 1993年 ,1994年 12月经中科院批准对外开放。实验室有多位我国计算机软件科学事业的开拓者 ,曾获得国家自然科学奖一、二、三等奖、国家科技进步奖二等奖、全国科学大会重大成果奖及何梁何利科技进步奖等。　　实验室学术委员会由 16名国内计算机科学界著名专家组成 ,董韫美院士任学术委员会主任。学术委员会在把握实验室研究方向等方面起到了重要作用。　　实验室现有固定人员 2 3人 ,林惠民院士任实验室主任。　　 2 0 0 2年实验室首次参加了科技部委托国家自然科学基金委员会…     

“不用归纳的归纳证明”与相对完备性

一、引言 一等式公理集确定了一个簇,即满足该公理集的全体模型。由一阶等式逻辑的完备性,等式e在一簇上为真,当且仅当应用等式推理规则,e从相应的公理集可证。在计算机科学的许多分支中,如抽象数据类型的代数描述及代数语义等,我们关心的不是满足一等式集的全体模型,而只是某一类特定的模型,如所谓初始模型。相对于这样的语义,等式推理规则不再完     

移动进程的空间逻辑

提出了一个用于描述异步π-演算中移动进程的时态和空间性质的模态逻辑. 该逻辑具有基于谓词变量的递归构造. 建立了这一逻辑的语义理论, 并证明了语义的单调性, 从而保证了不动点的存在. 还设计了一个算法来自动地检测移动进程是否具有用该逻辑公式所描述的性质, 并证明了该算法的正确性.     

多重继承的范畴论语义

Simula 67首先将类、次类、超类和继承的概念引入程序设计语言。这些思想在Smalltalk、C++等语言中得到了进一步的发展,形成了一种独特的、面向对象的程序设计风格。通过继承机制,次类可以共享超类中的代码,从而便利于增量式的软件开发方式,提高产品的可扩充性。 继承有单一和多重两种。单一继承即一个次类最多只能有一个直接超类,而在多重继承     

高级语言中的类型等价问题

本文针对强类型语言中的类型等价问题，研究了几个影响较大的高级语言对此问题的解决办法，讨论了结构等价与名字等价的利弊，进而分析了类型等价概念在高级语言中的作用，在此基础上，提出一个推荐方案，可以兼收结构等价与名字等价的长处，而不必付出额外的代价。本文最后对如何解决XYZ／G语言的类型等价规定提出了建议。     

网络技术与网络伦理

 2014年是中国接入互联网20年,截止到2013年底,中国网民规模达6.18亿。随着互联网的迅速普及,垃圾邮件、病毒、网络诈骗等问题也层出不穷,网络伦理成为一个需要着重探讨的话题。