类型系统λω×≤的PER模型

类型系统是近年来理论计算机科学的研究热点之一 .1999年周晓聪曾在文献 [1]中提出并研究了类型系统λω× ≤ 及其性质 .类型系统λω× ≤ 是λω×的扩充 ,引入了子类型关系和受限的全称类型 .与 System F的各种扩充相比 ,它区分各种上下文 ,使得规则和性质的研究更为清晰 .研究该类型系统的 PER模型作为其语义解释 ,并说明该模型的合理性  

一种用于指针程序安全性证明的指针逻辑

在高可信软件的各种性质中,安全性是被关注的重点,其中软件满足安全策略的证明方法是研究的热点之一.文中根据作者所设想的安全程序的设计和证明框架,为类C语言的一个子集设计了一个指针逻辑系统.该逻辑系统是Hoare逻辑系统的一种扩展,它用推理规则来表达每一种语句引起指针信息的变化情况.它可用来对指针程序进行精确的指针分析,所获得的信息用来证明指针程序是否满足定型规则的附加条件,以支持程序的安全性验证.该逻辑系统也可用来证明指针程序的其它性质.  

基于OPC的建筑管理系统集成研究

建筑管理系统(BMS)集成是智能建筑一体化集成的前提，但在BNS系统集成进程中却存在着严重障碍，即各子系统之间难以实现开放的、无缝隙的联接。OPC是与厂商无关的软件数据交换标准接口和规程，为解决这一问题提供了先进的技术手段。OPC技术保证了BMS系统集成的开放性。  

On model typing

Where object-oriented languages deal with objects as described by classes, model-driven development uses models, as graphs of interconnected objects, described by metamodels. A number of new languages have been and continue to be developed for this model-based paradigm, both for model transformation and for general programming using models. Many of these use single-object approaches to typing, derived from solutions found in object-oriented systems, while others use metamodels as model types, but without a clear notion of polymorphism. Both of these approaches lead to brittle and overly restrictive reuse characteristics. In this paper we propose a simple extension to object-oriented typing to better cater for a model-oriented context, including a simple strategy for typing models as a collection of interconnected objects. We suggest extensions to existing type system formalisms to support these concepts and their manipulation. Using a simple example we show how this extended approach permits more flexible reuse, while preserving type safety.  

移动计算系统信息流安全

程序信息流安全是信息安全的一个重要研究方向．基于类型的静态分析可以保证程序信息流安全与单进程系统相比．移动计算系统中数据通讯的存在使得程序信息流安全保护更加困难．Cornell大学的Zdancewic对函数式语言λsec的单进程程序信息流安全进行了研究．本文在其工作的基础上，根据移动计算系统的结构特征，通过对函数式语言λsec进行扩充，加入通讯原语，将其扩展成移动计算语言MobileML，并针对一个简单的移动计算模型，给出了描述程序信息流安全的无干扰性定义，设计了相应的信息流类型系统，用以静态检查保证MobileML语言程序信息流安全．  

一种带约束的多态类型系统

本文讨论了一种带约束的多态类型系统，引入了约束类型，约束与全称量化的结合使得参数化多态函数的应用更安全，同时也为重工的表示和实现提供了一个新的途径，提高了类型表示的抽象度。本文讨论的类型系统具有两个不同层次的类型结构，约束的引入与肖去是不同层次上的操作，最后，本文人出了类型检查算法Ｗｒ，并证明了此算法中约束的可满足性是可判定的。  

Validating a web service security abstraction by typing

An XML web service is, to a first approximation, an RPC service in which requests and responses are encoded in XML as SOAP envelopes, and transported over HTTP. We consider the problem of authenticating requests and responses at the SOAP-level, rather than relying on transport-level security. We propose a security abstraction, inspired by earlier work on secure RPC, in which the methods exported by a web service are annotated with one of three security levels: none, authenticated, or both authenticated and encrypted. We model our abstraction as an object calculus with primitives for defining and calling web services. We describe the semantics of our object calculus by translating to a lower level language with primitives for message passing and cryptography. To validate our semantics, we embed correspondence assertions that specify the correct authentication of requests and responses. By appeal to the type theory for cryptographic protocols of Gordon and Jeffrey's Cryptyc, we verify the correspondence assertions simply by typing. Finally, we describe an implementation of our semantics via custom SOAP headers. Received December 2003 Revised November 2004 Accepted December 2004 by A. E. Abdallah, P. Y. A. Ryan, S. A. Schneider and D. J. Cooke  

程序设计语言及相关领域的研究方向

本文主要讨论了程序设计语言的研究方向，以及与之有关的研究领域，并展望了程序设计语言的发展。  

Garment中多态类型的Ideal模型

本文从Ideal的基本概念出发,研究了Ideal作为类型的语义模型所具有的性质.在类型的Ideal模型下,讨论了Garment中参数化多态类型和约束多态类型的语义.并在此基础上,证明了Garment中类型规则的语义可靠性.  

具连续分布时滞的抛物型系统的变结构控制

基于比较原理,利用推广的向量Hanalay微分不等式,Dini导数,结合Green公式及不等式分析技术,研究一类具分布时滞的抛物型控制系统的变结构控制问题．首先对所导出的滑动模运动方程,在仅要求系数矩阵是个M-矩阵的条件下,获得了滑动模运动方程全局指数稳定性的充分条件,建立了滑动模运动方程全局指数稳定性定理．其次,设计了仅由状态函数描述的变结构控制器,给出了运动轨线到达滑动模态区的时间的估计．