程式語言理論

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

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

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

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

• 指称语义学，着重于语言的执行结果而非过程，包括域理论；

• 操作语义学，例如抽象机（象SECD抽象机），着重于描述语言的过程；

• 公理语义学，如 谓词变换语义学和代数语义学。

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

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

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

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

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

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

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