程式語言理論

编程语言理论（英語：Programming language theory）是计算机科学的一个分支，研究编程语言的设计、实现、分析、描述和分类及其各自的特点。它属于计算机科学，既依赖又影响着数学、软件工程、语言学，甚至认知科学。

λ演算在程式語言理論中有舉足輕重的地位，因此程式語言理論的非官方標誌是一個小寫的「λ」字母。

历史

从某种角度来看，编程语言理论的历史，甚至比编程语言本身的发展更久远。尽管阿隆佐·邱奇与斯蒂芬·科尔·克莱尼在1930年代发明的Lambda演算被一些人认为是世界上第一门编程语言，但其初衷是用于对计算进行建模，而不是作为一种程序员向计算机系统描述算法的手段。许多现代的函数式编程语言都声称自己是为Lambda演算提供了“一点包装”，并能轻松地以其解释。

世界上第一门编程语言是由康拉德·楚泽于1940年代设计的Plankalkül，但其直到1972年才广为人知，更是到1998年才被实现。Fortran则是第一门大获成功的高级编程语言，由约翰·巴科斯领导的IBM研究者们在1954-1957年间实现。Fortran的成功使一些科学家联合起来研究一种“通用的”计算机语言，并最终带来了ALGOL 58；麻省理工学院的约翰·麦卡锡则开发了Lisp，其为第一门源自学术界而取得成功的编程语言。随着1960年代这些起初的尝试获得成功，编程语言逐渐成为热门的研究对象，并延续至今。

子学科及相关领域

编程语言理论中存在着几个研究领域,或者对编程语言理论产生了深远的影响，其中许多有相当大的重叠。此外，PLT还利用了数学的许多其他分支,包括可计算性理论、类型论和集合论。

形式语义学

在计算理论中，形式语义学是关注计算的模式和程序设计语言的含义的严格的数学研究的领域。

语言的形式语义是用数学模型去表达该语言描述的可能的计算来给出的。

形式语义学（formal semantics），是程序设计理论的组成部分，以数学为工具，利用符号和公式，精确地定义和解释计算机程序设计语言的语义，使语义形式化的学科。

提供程序设计语言的形式语义的方法很多，其中主要类别有：

• 指称语义学，着重于语言的执行结果而非过程，包括域理论；
• 操作语义学，例如抽象机（象SECD抽象机），着重于描述语言的过程；
• 公理语义学，如 谓词变换语义学和代数语义学。

类型论

类型论提供了设计分析和研究类型系统的形式基础。实际上，很多计算机科学家使用术语“类型论”来称呼对编程语言的类型语言的形式研究，尽管有些人把它限制于对更加抽象的形式化如有类型lambda演算的研究。

程序分析

程序分析是指自动分析一个程序的包括正确性、健壮性、安全性和活跃性等特征的过程。 程序分析主要研究两大领域：程序的优化和程序的正确性。前者研究如何提升程序性能并且降低程序的资源占用，后者研究如何确保程序完成预期的任务。

比较程序语言分析

比较编程语言分析旨在根据编程语言的特点将其分类为不同类型，编程语言的大类通常被称为编程范型。

泛型和元编程

是指某类计算机程序的编写，这类计算机程序编写或者操纵其它程序（或者自身）作为它们的数据，或者在运行时完成部分本应在编译时完成的工作。

领域特定语言

指专注于某个应用程序领域的计算机语言。

编译原理

编译原理是编写编译器的理论。编译器的操作传统上分为语法分析(扫描和解析)、语义分析(确定程序应该做什么)、优化(根据某些指标改进程序的性能，通常是执行速度)和代码生成(用某种目标语言生成和输出等价的程序(通常是CPU的指令集)。

运行时系统

指一种把半编译的运行码在目标机器上运行的环境，介乎编译器及解释器的运行方式。包括虚拟机、垃圾回收和外部函数接口。