中文摘要：

任给一极小谓词演算可证正公式，对其全体证明的集合给出了一个半上下文无关文法描述。证明了该文法在下述意义下的完备性所给可证公式的任一证明，均可由相应的文法所产生的项模式所生成。该方法也可用于F系统和高阶逻辑等逻辑系统。建立了一个基于模式（scheme）的类型系统 - 模式演算。模式演算可以表示多种理论中的自然演绎证明。它与λ演算的主要区别在于无假设条件的命名。证明了模式演算与相应的类型λ演算具有同样的表达能力等性质。将R. Milner的顺序进程演算扩展为树进程演算，建立了一个可靠完备的推演系统。该系统描述了树进程之间的互模拟等价关系。提出了扩张互模拟的概念，用它给出了上下文无关文法进程间互模拟等价的一个有穷刻画。提出了弱分配域的概念。证明了对弱分配域而言MI∞成立和相应的Birkhoff-style定理。确立了ω-代数交cpos及其稳定函数空间的弱分配性之间的关系。为Plotkin的带常数传名调用λ-演算定义了一个新的CPS变换方法。在此基础上定义了CPS语言。建立了源语言和CPS语言的一一影射关系，并证明了Plotkin的模拟定理