λ演算是一个把函数当做方程式的理论，是一个把函数当做表达式操作的系统。它与可计算性、计算机科学、逻辑及数学等都有存在一定的联系。λ演算和图灵机是等价的。且它是函数编程语言的基础。此外，λ演算和逻辑系统也存在着奇妙的对应关系，这种对应关系称为Curry-Howard同构。还可以利用λ演算构造各种不同的数学模型。因此，对λ演算的研究，对计算理论、程序语言设计、逻辑及数学等都有重要的意义。　　标准化、Church-Rosser定理、规格化、分离属性等是λ演算的重要性质。类型λ演算是在λ演算基础上为每个术语赋予一个类型，最初为λ演算提出的类型系统是简单类型。但在简单类型系统中，有些术语是不可类型的，如不能为λx.xx分配类型，因此出现了交类型。交类型是简单类型的扩展，交类型系统可以为在简单类型系统中不可类型的术语赋予类型。交类型首次被提出是为了对λ术语的强标准化进行逻辑描述，此后被用来证明λ演算的各种性质。目前为止，λ演算已有很多变种，如Λμ，λGtz是λ演算在Curry-Howard同构方向上提出的扩展演算。Λμ演算是λμ的扩展，而λμ和经典自然演绎是Curry-Howard同构的。λGtz演算和直觉主义相继式演算LJ是同构的。本文把注意力放在Λμ演算和λGtz演算的标准化性质上。本文的工作有:　　1.λ演算的标准化定理声明最左规约策略是标准化的，且常用于证明一个术语不存在范式。该定理首次由Curry证明，Curry的证明基于Church-Rosser定理和规格化定理，而这两个定理的证明也相当复杂。在本文给出了另一种只基于类型系统简单性质的方法。本文使用交类型系统验证了标准化定理，并展示了在特定交类型系统中，如果能为术语M分配类型，那么M的最左规约是标准化的。　　2.Λμ是为了修复λμ的分离属性而提出的，分离属性被Saurin证明。本文使用交类型和积类型为Λμ演算定义了类型系统。并证明了在该系统中，术语在规约过程中保持类型不变，同时本文为Λμ定义了永久规约策略，当M能够永久规约到N时，若知道N的类型为A，那么M的类型也为A。此外，本文还证明了Λμ演算的术语是强标准化的当且仅当该类型系统可以为它分配类型。　　3.交类型系统根据类型是否满足A∩A=A分为幂等交类型系统和非幂等交类型系统。他们已经在自然演绎系统中得到广泛应用，但没有针对相继式演算的非幂等类型系统出现。使用幂等交类型系统得到描述结论常依赖于可约性方法，或通过PSN(Preservation Strong Normalization)性质将一个已知结论的中间演算的描述迁移到新的扩展演算上，这两种方法通常比较复杂或不够直接。本文为λGtz演算定义了非幂等交类型系统。λGtz是一个相继式演算。本文直接证明了λGtz术语在该类型系统中可接收类型当且仅当是强标准化的。利用非幂等系统证明术语的强标准化性质仅依赖于一个数字度量的递减性，这种证明方法更简单。