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

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

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

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

In programming language theory, semantics is the field concerned with the rigorous mathematical study of the meaning of programming languages. It does so by evaluating the meaning of syntactically legal strings defined by a specific programming language, showing the computation involved. In such a case that the evaluation would be of syntactically illegal strings, the result would be non-computation. Semantics describes the processes a computer follows when executing a program in that specific language. This can be shown by describing the relationship between the input and output of a program, or an explanation of how the program will execute on a certain platform, hence creating a model of computation.