New development in the matured linear logic research and its applications

线性逻辑证明理论和语义理论已经发展起来，研究已经达到了证明理论和语义理论相结合的成熟阶段。在这个项目中，我们开发了一种整合线性逻辑和相关逻辑的证明理论和语义的方法。我们特别开发了一种利用这一集成框架来研究证明理论性质的方法，利用一种阶段语义技术，包括“简单逻辑”与线性逻辑的关系、切除的统一和抽象表征以及逻辑计算模型。我们还将线性逻辑语法和语义应用于实时系统设计的形式化验证技术和安全协议的正确性证明技术，以及编程语言的计算复杂性理论和类型推理理论。

Linear logical proof theory and semantics theory have been developed and the researches have reached a matured stage to integrate proof theory and semantics theory. In this project we developed a method of integrating proof theory and semantics of linear logic and related logics.We specially developed a method to study proof theoretic properties using this integrated framework, by using a phase semantic techniques, including the relation between "simple logic" and linear logic, uniform and abstract characterizations of cut-eliminations and logical computation models.We also applied the linear logical syntax and semantics to formal verification techniques on real-time system designs and correctness proof techniques on security protocols as well as to computational complexity theory and type-inference theories for programming languages.