プログラミング言語の基礎概念(プログラミング ゲンゴ ノ キソ ガイネン)

普段コードを書いていると「型が合わない」「評価順序が違う」といった現象に遭遇しますが、それらを厳密に説明できるかと問われると言葉に詰まることがあります。本書はプログラミング言語の振る舞いを操作的意味論、型システムという道具立てで形式的に記述する方法を教える、計算機科学の入門的教科書です。京都大学の講義を母体にしており、導出木を使って「プログラムが値を返す」という事実を証明のように組み立てる独特のアプローチを取ります。

大きな特徴は、オンライン演習システム (CoPL) が用意されている点です。導出木を手で構築して提出すると正誤判定が返るため、紙の上の理論が「解ける問題」に変わり、抽象的な定義を実感として掴みやすくなります。扱う言語機能は整数演算からリスト、パターンマッチ、多相型まで段階的に広がり、言語設計者がどのように構文と意味を対応付けているかを追体験できます。

前提知識としては集合と論理の基礎があれば読み進められますが、数学的な推論に慣れていないと導出規則の記法に戸惑うかもしれません。プログラミング言語そのものの成り立ちを理解したい人、あるいはコンパイラや型検査器の仕組みに関心がある人にとって、理論への確かな足場を築いてくれる一冊です。