読んだ計算機科学の教科書を記録していきます
| Title | Author | Publisher | Date | Comments |
|---|---|---|---|---|
| Mathematical Logic | Joseph R. Shoenfield | Addison Wesley Longman | 1967/12 | 数理論理学の入門書 |
| The Formal Semantics of Programming Languages | Glynn Winskel | MIT Press | 1993 | 意味論の解説書 |
| Symbolic Logic and Mechanical Theorem Proving | Chin-Liang Chang Richard Char-Tung Lee | Academic Pr | 1973/06/15 | First Order Logicの解説書 |
| Modern Compiler Implementation in ML | Andrew W. Appel | Cambridge University Press | 2004/07/08 | MLでのコンパイラーの仕組み |
| communicating and mobile systems:the pi-calculus | Robin Milner | Cambridge Univ Pr | 1999/06/15 | pi-calculusの解説書 |
| 計算論 計算可能性とラムダ計算 | 高橋正子 | 近代科学社 | 1991/08 | 型なしλ計算の入門書 |
| Types and Programming Languages | Benjamine C. Pierce | MIT Press | 2002/02/01 | 型付きλ計算の入門書 |
| Logic and Structure | D. van Dalen | Springer-Verlag | 2004 | 一階述語論理の証明論、モデルの理論の入門書。 |
| Proofs and Types | J.-Y. Girard, Y. Lafont and P. Taylor | Cambridge University Press | 1989 | 証明論、型理論とその意味論 |
| Recursion Theory | Joseph R. Shoenfield | A K Peters Ltd | 2001/01/15 | Recursion Theory |
| 様相論理入門 | G.E.ヒューズ M.J.クレスウェル | 恒星社厚生書閣 | 1981 | 様相論理学の入門書 |
| Handbook of proof theory | Buss | North-Holland | 1998 | 証明論、Realizability |
| Categories for Types | Roy L. Crole | Cambridge University Press | 1993 | category theoryの入門からType theoryまで |
| Introduction to higher order categorical logic | J.Lambek and P.J.Scott | Cambridge University Press | 1986 | ひたすら圏論、難しい |
| Semantics and Logics of Computation | A.Pitts and P.Dybjer | Cambridge University Press | 1997 | ゲーム感覚で読める |
| 数学ワンポイント双書 無限集合 | 森毅 | 共立出版 | 1976 | 文章面白い、選択公理とパラドックス |
| 臨時別冊・数理科学 SGCライブラリ 43 アルゴリズムと計算量 | 谷聖一 | サイエンス社 | 1987 | ＰとＮＰについて |
| 2006年5月 | ||||
| セクシーな数学 | グレゴリー・Ｊ・チャイティン 黒川利明訳 | 岩波書店 | 2003年 | チャイティンの自慢話 |
| 知の限界 | グレゴリー・Ｊ・チャイティン 黒川利明訳 | SBACCESS | 2001年 | チャイティンの数学概観 |
| 数学の限界 | グレゴリー・Ｊ・チャイティン 黒川利明訳 | SBACCESS | 2001年 | LISPによる不完全性定理の再証明 |
| ゲーデル,エッシャー,バッハ―あるいは不思議の環 | ダグラス・R・ホフスタッター (著) 野崎 昭弘 はやしはじめ 柳瀬尚紀(訳) | 白揚社 | 1985年 | 765ページの大著。人間にできることの記述への挑戦。 |
| 型理論 | 龍田真 | 近代科学者 | 1992年 | Type Theoryの日本語での入門書 |
| 集合とはなにか | 竹内外史 | 講談社ブルーバックス | 2001年 | 公理的集合論の平易な解説 |
| ゲーデルは何を証明したか | ナーゲル、ニューマン著 林一訳 | 白揚社 | 1999年 | 不完全性定理の歴史的意味 |
| 数学基礎論入門 | 前原昭二 | 朝倉書店 | 1977年 | 基礎論＋帰納的関数、不完全性定理が丁寧 |
| 数理論理学 | 林晋 | コロナ社 | 1989年 | 論理学、標準化定理、sequent calculus、分解原理など |
| 2006年6月 | ||||
| 帰納的関数 | 廣瀬健 | 共立出版 | 1989年 | recursion theoryの入門書、degreeが簡単に |
| Proof theory and logical complexity | Girard | North-Holland | 1990年 | girard流の書き方が面白いってことで読もうと思ったけど、読めずじまい |
| 2006年7月 | ||||
| Semantics and Logics of Computation | Pitts, Andrew M | CAMBRIDGE UNIVERSITY PRESS | 1997年 | カテゴリーとgame semantics |
| 2006年8月 | ||||
| Computable Analysis | Klaus Weihrauch | Springer | 1998年 | 実数上のcomputability |
| 2006年9月 | ||||
| Classical Recursion Theory | P.Odifreddi | North-Holland | 1999年 | recursion theoryのハンドブック |
| Classical Recursion Theory VolumeⅡ | P.Odifreddi | North-Holland | 1999年 | recursion theoryのハンドブック |
| Computability Theory | S.Barry Cooper | A CRC Press Company | 2002年11月 | Computability Theoryを短くまとめたもの |
| Title | Author | Journal articles | Comments | |
|---|---|---|---|---|
| Approximate and Limited Reasoning | Finger, M. and R. Wassermann. | Journal of Logic and Computation, 2004 | 制限のある論理 | |
| Proof theory in the abstract | J.M.E. Hyland | Annals of Pure and Applied Logic 114 (2002) 43-78 | 圏論での証明論解釈 | |
| Diagonal Arguments and Cartesian Closed Categories | F.William Lawvere | Theory and Applications of Categories, No.15,2006,pp.1-13 | パラドックスを不動点定理によってまとめた | |
| Self-Reference and Fixed Points: A Discussion and an Extension of Lawvere's Theorem | Jorge Soto-Andrade and Francisco J.Varela | Acta Applicandae Mathematicae 2,1-19. | Lawvereの定理の逆 | |
| Cantor Diagrams: A Unifying Discussion of Self-Reference | G.M.Germano and S.Mazzanti | Applied Categorical Structures 11:313-336,2003 | Lawvereの定理の具体例を２種類に分類 | |
| A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points | Noson S.Yanofsky | arXiv:math.LO/0305282v1 19 May2003 | categoryを使わずに関数で書き直した | |
| 自己言及の論理と計算 | 長谷川真人 | Homepageより | 前半は自己言及と対角線論法、後半は自己言及現象の自明でないモデル | |
| 2006年5月 | ||||
| ゲーデルを超えて オメガ数が示す数学の限界 | チャイティン | 日経サイエンス2006年6月号 | 計算できない数オメガについて | |
| A Simplification of Girard's Paradox | Antonius J.C. Hurkens | Lecture Notes In Computer Science; Vol.902, Pages:266-278 | Girard's Paradoxのまとめ | |
| An Analysis of Girard's Paradox | Theierry Coquand | LICS 1986 | Girard's Paradoxのまとめ | |
| The Computational Behaviour of Girard's Paradox | Douglas J. Howe | LICS 1987 | Girard's Paradoxの項の解析 | |
| 2006年6月 | ||||
| Introduction to generalized type systems | HENK BARENDREGT | Journal of Functional Programming 1(2):125-154,April 1991 | ラムダキューブの説明 | |
| Nontions of computability at higher types1 | John R. Longley | 2003, Association for symbolic logic | higher typeのcomputabilityについて | |
| 再帰関数論 | 照井一成 | recursion theoryからみた不完全性定理、logicより | ||
| 算術的階層の厳密性と形式的手法の限界について | 照井一成 | arithmetical hierarchyについて | ||
| computability and recursion | Robert I. Soare | recursion theoryではなく、computability theoryと言おうという話 | ||
| Three Theorems on Recursive Enumeration.1.Decomposition.2.Maximal Set.3.Enumeration Without Duplication | Richard M. Friedberg | The Journal of Symbolic Logic, Vol.23, No.3.(Sep.,1958),pp.309-316 | 1はc.e. setがdisjointな2つのc.e. setのunionという定理 | |
| Program size, oracles, and the jump operation | Gregory J. Chaitin | Osaka Journal of Mathematics 14 (1997), pp.136-149 | ||
| 2006年7月 | ||||
| Chaitin Ω Numbers, Solovay Machines, and Incompleteness | Cristian S. Calude | CDMTCS-114 | computable real | |
| Chaitin Ω Numbers and Strong Reducibilities | Cristian S. Calude | CDMTCS-062 | computable real | |
| 2006年8月 | ||||
| Relativizing Chaitin's halting probability | Rod Downey | Journal of Mathematical Logic, Vol. 5, No.2(2005) 167-192 | computable real |