在編程語言理論中，語義學是對編程語言含義的嚴格數學研究。 語義為編程語言語法中的有效字符串分配計算意義。

語義描述了計算機在以該特定語言執行程序時遵循的過程。 這可以通過描述程序的輸入和輸出之間的關系，或解釋程序將如何在特定平臺上執行來顯示，從而創建計算模型。

1967 年，羅伯特·W·弗洛伊德 (Robert W. Floyd) 發表了論文 Assigning meanings to programs； 他的主要目標是為計算機程序的證明制定嚴格的標準，包括正確性、等價性和終止性的證明。 弗洛伊德進一步寫道：

在我們的方法中，編程語言的語義定義是建立在句法定義之上的。 它必須指定語法正確的程序中哪些短語代表命令，以及必須對每個命令附近的解釋施加什么條件。

1969 年，托尼·霍爾 (Tony Hoare) 發表了一篇關于以弗洛伊德 (Floyd) 思想為種子的霍爾邏輯的論文，現在有時統稱為公理語義學。

在 1970 年代，出現了操作語義和指稱語義這兩個術語。

形式語義學領域包括以下所有內容：

• 語義模型的定義
• 不同語義模型之間的關系
• 不同意義處理方法之間的關系
• 邏輯、集合論、模型論、范疇論等領域的計算與底層數學結構之間的關系。

它與計算機科學的其他領域有密切聯系，例如編程語言設計、類型理論、編譯器和解釋器、程序驗證和模型檢查。

形式語義有很多方法； 這些屬于三大類：

• 外延語義，語言中的每個短語都被解釋為外延，即可以抽象地思考的概念意義。 這樣的外延通常是居住在數學空間中的數學對象，但并不要求它們必須如此。 作為一種實際需要，外延是使用某種形式的數學符號來描述的，這又可以形式化為指稱元語言。 例如，功能語言的指稱語義通常將語言翻譯成領域理論。 指稱語義描述還可以作為從編程語言到指稱元語言的組合翻譯，并用作設計編譯器的基礎。
• 操作語義，直接描述語言的執行（而不是通過翻譯）。 操作語義松散地對應于解釋，盡管解釋器的實現語言通常也是一種數學形式。 操作語義可以定義一個抽象機器（例如 SECD 機器），并通過描述它們在機器狀態上引起的轉換來賦予短語意義。 或者，與純 lambda 演算一樣，可以通過對語言本身的短語進行句法轉換來定義操作語義；
• 公理語義學，通過描述適用于短語的公理來賦予短語意義。 公理化語義不區分短語的含義和描述它的邏輯公式； 它的意義正是在某種邏輯上可以證明的。 公理語義的典型例子是霍爾邏輯。

除了在指稱、操作或公理化方法之間進行選擇外，形式語義系統的大多數變化都來自支持數學形式主義的選擇。

形式語義的一些變體包括：

• • 動作語義是一種嘗試模塊化指稱語義的方法，將形式化過程分為兩層（宏語義和微觀語義）并預定義三個語義實體（動作、數據和 yielders）以簡化規范；
  • 代數語義是基于代數定律的公理語義的一種形式，用于以形式化的方式描述和推理程序語義。 它還支持指稱語義和操作語義；
  • 屬性語法定義了系統地為語言句法的各種情況計算元數據（稱為屬性）的系統。 屬性語法可以理解為一種指稱語義，其中目標語言只是原始語言，并通過屬性注釋進行了豐富。 除了形式語義之外，屬性語法還被用于編譯器中的代碼生成，以及使用上下文敏感條件來擴充常規或上下文無關語法。