在計算理論中，形式語義學是關注計算的模式和程序設計語言的含義的嚴格的數學研究的領域。
語言的形式語義是用數學模型去表達該語言描述的可能的計算來給出的。
形式語義學（formal semantics），是程序設計理論的組成部分，以數學為工具，利用符號和公式，精確地定義和解釋電腦程式設計語言的語義，使語義形式化的學科。
提供程序設計語言的形式語義的方法很多，其中主要類別有：
