
関連サイト
本書の関連ページが用意されています。
内容紹介
型システムとは、プログラミング言語の安全性や効率を高めるうえで重要な理論・手法です。本書は、その型システムについて基礎的な話題を網羅し、実装例を交えて丁寧に解説したThe MIT Press発行の解説書“Types And Programming Languages”(TAPL)を翻訳したものです。言語設計者や学生だけでなく、静的型付言語を深く理解して活用したいプログラマーにとっても貴重な情報となっています。
書誌情報
- 著者: Benjamin C. Pierce(著), 住井英二郎(監訳), 遠藤侑介, 酒井政裕, 今井敬吾, 黒木裕介, 今井宜洋, 才川隆文, 今井健男(訳)
- 発行日: 2014-04-10 (紙書籍版発行日: 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 ではじめる形式手法』(共訳、オーム社)。
目次
日本語版に寄せて
監訳者序文
- 実用的情報
序文
- 謝辞