在计算理论中，形式语义学是关注计算的模式和程序设计语言的含义的严格的数学研究的领域。
语言的形式语义是用数学模型去表达该语言描述的可能的计算来给出的。
形式语义学（formal semantics），是程序设计理论的组成部分，以数学为工具，利用符号和公式，精确地定义和解释计算机程序设计语言的语义，使语义形式化的学科。
提供程序设计语言的形式语义的方法很多，其中主要类别有：
