試験公開中

このエントリーをはてなブックマークに追加

型システム入門 プログラミング言語と型の理論

オーム社

5,440円+税

型システムを理解するうえでの定番書を翻訳

関連サイト

本書の関連ページが用意されています。

内容紹介

型システムとは、プログラミング言語の安全性や効率を高めるうえで重要な理論・手法です。本書は、その型システムについて基礎的な話題を網羅し、実装例を交えて丁寧に解説したThe MIT Press発行の解説書“Types And Programming Languages”(TAPL)を翻訳したものです。言語設計者や学生だけでなく、静的型付言語を深く理解して活用したいプログラマーにとっても貴重な情報となっています。

書誌情報

  • 著者: Benjamin C. Pierce(著), 住井英二郎(監訳), 遠藤侑介, 酒井政裕, 今井敬吾, 黒木裕介, 今井宜洋, 才川隆文, 今井健男(訳)
  • 発行日: (紙書籍版発行日: 2013-03-29)
  • 最終更新日: 2014-04-10
  • バージョン: 1.0.0
  • ページ数: 528ページ(PDF版換算)
  • 対応フォーマット: PDF
  • 出版社: オーム社

対象読者

情報科の学生、研究者 静的型付言語を利用するプログラマー

著者について

Benjamin C. Pierce

Pennsylvania 大学計算機・情報科学科教授(Salvatori Professor)。主な研究分野はプログラミング言語、静的型システム、ソフトウェアセキュリティ、並行・分散プログラミング、および同期技術。著書に “Types and Programming Languages”(本書)、“Software Foundations” などがあり、大学院の教科書として幅広く用いられている。多くの一般ユーザを持つファイル同期ソフトウェア Unison のメイン設計者でもある。

住井英二郎

1998年東京大学理学部情報科学科卒業。2000年 Pennsylvania 大学 Visiting Scholar。2001年東京大学大学院情報理工学系研究科コンピュータ科学専攻助手(同情報学環流動教員)。2003年 Pennsylvania 大学Research Associate。2004年東京大学大学院博士(情報理工学)。2005年東北大学大学院情報科学研究科助教授(2007年同准教授)、現在に至る。日本学術振興会賞、日本 IBM 科学賞、マイクロソフトリサーチ日本情報学研究賞等受賞。日本学術会議特任連携会員。未踏ソフトウェア創造事業スーパークリエータ。

遠藤侑介

2006 年東京大学大学院情報理工学系研究科修士課程修了。現在、株式会社 東芝 研究開発センター勤務。プログラミング言語、分散データベースに関する研究開発に従事。趣味は Ruby プログラミング言語の開発、関東の鉄道の沿線ウォーキング。訳書に『抽象によるソフトウェア設計 — Alloy ではじめる形式手法』(共訳、オーム社)。

酒井政裕

2007年慶應義塾大学大学院政策・メディア研究科修士課程修了。現在、株式会社 東芝 研究開発センター勤務。形式手法、ソフトウェアテストなどのソフトウェア高信頼化の研究に従事。関数的プログラミングや理論計算機科学にも興味を持つ。訳書に『抽象によるソフトウェア設計 — Alloy ではじめる形式手法』(共訳、オーム社)。

今井敬吾

2009年名古屋大学大学院情報科学研究科博士後期課程単位取得退学。博士(情報科学)。2007年 同研究科附属組込みシステム研究センター研究員、2010年より有限会社 IT プランニング勤務。π 計算など並行計算の型システムに興味を持つ傍ら、実務では OCaml や Haskell を用いたソフトウェア開発を行う。

黒木裕介

2007年東京大学大学院情報理工学系研究科修士課程修了。現在、株式会社 東芝 研究開発センター勤務。スケジューリングなどの研究開発に従事(専門は数理最適化)。他に、TEX ユーザの集い 2009–2012 や TUG 2013(第 34 回 TEX Users Group 年次大会)で実行委員を務める。

今井宜洋

2007年名古屋大学大学院多元数理科学研究科博士課程前期課程修了。現在、有限会社 IT プランニング勤務。関数型プログラミング言語や証明支援系 Coq を使ったシステム開発に従事。証明系に関する勉強会 ProofCafeを主催する他、トップエスイーの講師を務める。

才川隆文

2011年名古屋大学大学院多元数理科学研究科博士課程前期課程修了。現在、同後期課程在学。型理論など計算機科学と、関連する数学を研究。趣味は型無しの理論や言語。

今井健男

2000年東京大学大学院理学系研究科修士課程修了。現在、株式会社 東芝 研究開発センター勤務。形式手法、ソフトウェアテストなどのソフトウェア高信頼化の研究に従事。訳書に『抽象によるソフトウェア設計 —Alloy ではじめる形式手法』(共訳、オーム社)。

目次

日本語版に寄せて

監訳者序文

  • 実用的情報

序文

  • 謝辞

第1章 はじめに

第2章 数学的準備

■第1部 型無しの計算体系

第3章 型無し算術式

第4章 算術式のML実装

第5章 型無しラムダ計算

第6章 項の名無し表現

第7章 ラムダ計算のML実装

■第2部 単純型

第8章 型付き算術式

第9章 単純型付きラムダ計算

第10章 単純型のML実装

第11章 単純な拡張

第12章 正規化

第13章 参照

第14章 例外

■第3部 部分型付け

第15章 部分型付け

第16章 部分型付けのメタ理論

第17章 部分型付けのML実装

第18章 事例:命令的オブジェクト

第19章 事例:Featherweight Java

■第4部 再帰型

第20章 再帰型

第21章 再帰型のメタ理論

■第5部 多相性

第22章 型再構築

第23章 全称型

第24章 存在型

第25章 System F のML実装

第26章 有界量化

第27章 事例:命令的オブジェクト再考

第28章 有界量化のメタ理論

■第6部 高階の型システム

第29章 型演算子とカインド

第30章 高階多相

第31章 高階部分型付け

第32章 事例:純粋関数的オブジェクト

付録A 演習の解答

付録B 記法

参考文献

訳語集

規則図一覧

索引

Home 書籍一覧 型システム入門 プログラミング言語と型の理論 ▲ ページトップへ戻る