基于进程演算的程序语言设计与实现能够将并发理论的语法和语义理论研究真正应用于实践，并从根本上用高效的并发计算去替代传统的顺序计算，这是研究进程演算的一个关键问题。本文从经典的顺序函数式类型程序语言出发，层层深入地考虑现有成熟的程序语言与传值进程演算之间的关系。首先，本文把PCF（编程可计算函数式语言）作为最初的切入点，去讨论程序语言之间的表达能力关系，如果有了一个语法类型系统更简单而且表达能力足够强的语言，那么就便于去研究与进程演算之间的关系；进一步的，在PCF的基础上，本文讨论并发高性能的函数式语言，研究其与进程演算之间的表达能力关系，这对于进程演算的应用价值将会有更深的体现，对进程演算中的理论研究结果也将有更直观的认识。　　进程演算中现有应用于程序语言的工作，主要是集中在π演算上，该传名进程演算对于通信相对抽象。在程序语言的实现中也存在语法和等价关系的问题，现在基于π演算的程序语言性能上还有很大的不足，都需要更多的工作来找合适的进程演算模型和等价关系，以促进进程演算在程序语言中的应用。　　本文工作的主要贡献主要分为三个方面：　　1.通过在按值归约PCF引入完备和可判定的一阶理论Presburger算术，本文提出了一个类型系统更简单的语言PCFLC。从递归函数定义和程序语言表达能力两方面来研究了PCFLC和按值归约PCF的关系：递归函数定义方面，本文提出一个了PCF的极小化模型，给出了函数阶的概念，并且证明了任意函数阶的项都可以在PCFLC中定义出来；程序语言表达能力方面，定义了类型程序语言中的值应用互模拟等价关系，给出了一个从按值归约PCF到PCFLC的编码，这个编码对于值应用互模拟是完全抽象的，这部分工作表明了PCFLC和按值归约PCF在操作语义上有相同的表达能力，而其语法简单可以做为一个中间模型来比较程序语言的表达能力。　　2.进程演算中实际应用最多的模型是π演算，但现有π演算中的等价关系大多不适用于类型函数式语言的验证，并且对于无限值的编码也缺乏效率。传值进程演算虽然抽象性低于π演算，但有很好的方法来解决这些问题。因此本文提出了一个传值进程演算的变种VPCΣ，并且引入了很多内置的函数来使其对于实际程序的验证和分析更加有效，然后给出了其的符号操作语义，并研究了VPCΣ的表达能力。　　3.提出了一个VPCΣ中的通用解释程序语言解释框架。在此框架下，对并发函数式语言Erlang的核心语义进行了解释，并给出正确性的证明，主要包括：参照Erlang及其核心部分core Erlang的手册归规范形式化了该语言的操作语义；对于core Erlang语言，给出了一个VPCΣ中结构化的解释；证明了形式化操作语义和本文解释之间在迟符号互模拟关系下满足操作一致性，这对Erlang形式化工作一个非常好的性质。而前人的工作中因为π演算中存在的问题大多没有办法给出这方面的结果，本文用一个并行通信的实例进行了说明。　　总的来说，本文主要研究了如下问题：函数式语言中等价关系、表达能力关系；传值进程演算的表达能力；传值进程演算对并发函数式程序语言的通用解释和正确性证明，这些工作保证了程序分析的可靠性。本文的工作对于进程演算有很好的指导意义，即便不具有π演算的传名能力，传值进程演算仍然可以作为一个抽象层面稍低的演算，并利用其中的语法和语义结果来指导并发函数式语言的实现，本文可以对传值进程演算和传名进程演算的解释能力进一步的进行研究，以便对基于进程演算的程序语言设计有更深入的了解。