プログラムは記号であり、したがって「意味」を持ちます。
とくにプログラムを厳密に分析するためには、形式的に(=機械的に操作可能な形式で)意味を記述する必要があります。
たとえばコンパイラによる最適化処理の正しさは、元のプログラムと最適化後のプログラムの意味が同一であることを証明して初めて確実といえます。

形式的意味論のうち操作的意味論と(Hoare流)公理的意味論は、プログラム実行前後の変化を明示して意味とします。

もう一つの表示的意味論はプログラムに数学的存在を対応させて意味とします。
数学的存在とは数学による形式化が可能な概念をいいます。
"123"というコードは整数123を意味し、数学の形式で"123"と書きます。
"int f(int x){return x+1;}"というコードは引数に１を加えて返す関数を意味し、数学では"f : x |-> x + 1"と表現します。

問題は「汎用」プログラミング言語に現れる再帰的構造です。
無限につづく計算過程が再帰によって生じます。
結果を返すことのない無限再帰は、無意味です。
しかしプログラミング言語のチューリング完全性とも呼ばれる汎用性は、まさにこの無限再帰の上に成立しています。
そのため無意味な無限再帰にも意味を与えなければなりません。

無限集合や無限小など、数学にも無限は現れます。
パラドクスや不完全性定理による動揺を乗り越え、数学はこれらの危険で有益な無限を形式化する術を洗練させました。
そして表示的意味論は、数学が発展させた領域論や圏論をもちいて、再帰から生じる無限を形式化します(※本書で圏論は扱いません)。

表示的意味論は抽象的で難解ですが、本書は定理証明が丁寧で比較的理解できる難易度です。
類書を易しいものから並べると
コンピュータサイエンス入門
プログラム意味論
本書
Semantics of Programming Languages
でしょうか。
ちなみに私は本書を大堀淳先生から紹介されました。その点でもおすすめできます。