摘要： 线性和为一种动作逻辑，有很强的表达能力和很中构造性，线性逻辑式程序设计语言为表达操作语义，并发现规范等提供了新的工具和框架，Ｇｉｒａｒｄ对线性逻辑所作的“定义”概念的扩充对状态变迁系统中模拟和双模拟提供了证明论框架，本文论述了这方面的成果。

关键词: 证明论 并发变迁系统 线性逻辑 程序设计