プログラミング言語の形式的意味論入門

ウィンスケル，Ｇ．【著】〈Ｗｉｎｓｋｅｌ，Ｇｌｙｎｎ〉/末永 幸平【監訳】/勝股 審也/中澤 巧爾/西村 進/前田 敦司【訳】

丸善出版（2023/01発売）

• サイズ A5判／ページ数 316p／高さ 21cm
• 商品コード 9784621307632
• NDC分類 007.1
• Cコード C3004

出版社内容情報

プログラミング言語の（形式的）意味論とは、プログラムの動作を数学によって厳密に定義し、その性質について議論するための枠組みのことである。プログラムを数学の俎上に載せることにより、プログラムやプログラミング言語を厳密に理解し、解析し、これらについて推論することができるようになる。この分野は近年実用化に向けて進んでいる形式手法の礎となり、またそれ自体、様々な数学概念が飛び交う興味深い一分野を形成してきた。

本書は、Winskelによるプログラミング言語意味論の世界的標準教科書の邦訳である。前提知識をできるだけ少なくしつつ、プログラムの意味を数学的に定義・議論するための手法が解説されている。本書により、プログラミング言語理論関係の専門的な文献を読むための基礎を学ぶことができる。本書で身につけた基礎知識は、プログラミング言語研究の成果を理解し応用するために役立つはずである。

内容説明

本書は、Ｗｉｎｓｋｅｌによるプログラミング言語意味論の世界的標準教科書の邦訳である。前提知識をできるだけ少なくしつつ、プログラムの意味を数学的に定義・議論するための手法が解説されている。本書により、プログラミング言語理論関係の専門的な文献を読むための基礎を学ぶことができる。本書で身につけた基礎知識は、プログラミング言語研究の成果を理解し応用するために役立つはずである。

目次

集合論の基礎
入門：操作的意味論
帰納法の原理
帰納的な定義
ＩＭＰの表示的意味論
ＩＭＰの公理的意味論
ホーア規則の完全性
領域理論入門
再帰方程式
再帰の技法
高階型を持つ言語
情報システム
付録Ａ　不完全性と決定不能性

著者等紹介

末永幸平［スエナガコウヘイ］
京都大学大学院情報学研究科准教授

勝股審也［カツマタシンヤ］
国立情報学研究所特任准教授

中澤巧爾［ナカザワコウジ］
名古屋大学大学院情報学研究科准教授

西村進［ニシムラススム］
京都大学大学院理学研究科准教授

前田敦司［マエダアツシ］
筑波大学システム情報系准教授（本データはこの書籍が刊行された当時に掲載されていたものです）
※書籍に掲載されている著者及び編者、訳者、監修者、イラストレーターなどの紹介情報です。

感想・レビュー

※以下の感想・レビューは、株式会社ドワンゴの提供する「読書メーター」によるものです。

[Q]

ある程度理想的なプログラムを形式的に解釈する本。おそらく大学レベルの教科書向けに書かれているので、それなりの難易度。自作言語を作っていて、その証明部分の機能を作る手掛かりが欲しくて手に取った。実直な感想として本書のような理論的背景、さらには現実的な副作用コミコミのプログラムへ本書のような意味論を組み込むのはそれだけで巨大な研究テーマになってしまうとやはり感じる。LeanやRocq(Coq)のような既存の証明器やZ3などのソルバを使えるようなプログラム構造に最初から目指した方が良い。

2026/06/24

[takao]

ふむ

2024/11/24