経歴

学歴・職歴

その他


社会的活動

所属学会

学術誌編集委員

組織委員・プログラム委員(国際会議のみ)

その他


業績

著書

  1. PX: A Computational Logic, S. Hayashi and H. Nakano,1988, The MIT Press, free PDF volume
  2. 数理論理学, 平成元年12月, コロナ社
  3. 続・新しいプログラミング・パラダイム, 平成2年11月, 共立出版, 分担執筆
  4. 現代数理科学辞典, 平成3年3月, 大阪書籍, 分担執筆
  5. 構成的プログラミングの基礎 , 平成3年4月, 遊星社, 林晋・小林聡
  6. 情報系の数学入門 , 平成5年9月, オーム社, 林晋・八杉満利子
  7. ゲーデルの謎を解く , 平成5年11月, 岩波書店
  8. コンピュータ基礎理論ハンドブック, 8章「プログラミング言語における型理論」担当, 平成6年, 丸善出版, 分担訳
  9. プログラム検証論 , 平成7年9月, 共立出版
  10. 「論理パズルとパズルの論理」, 八杉満利子・ 林晋, 平成10年9月, 遊星社
  11. 「パラドックス!」林晋編著、平成12年8月, 日本評論社
  12. 「お話・数学基礎論」八杉満利子・林晋、平成14年6月20日, 講談社
  13. 「不完全性定理」K. ゲーデル著、林晋・八杉満利子訳と解説、平成18年9月15日、岩波書店、岩波文庫
    正誤表
  14. 渕一博―その人とコンピュータサイエンス, 田中穂積他著, 近代科学社, 2010年3月, 257頁, 分担執筆, 担当第1部,第1章.

主な学術論文(査読論文・招待論文)

  1. On derived rules of intuitionistic second order arithmetic 1977,Commentariorum Mathematicorum Universitatis Sancti Pauli, XXVI, pp.77-103
  2. A note on provable well-orderings in first order systems with infinitary inference rules, 1977,Tsukuba Journal of Mathematics, vol.1, pp.125-135
  3. Existence property by means of a normalization method, 1978, Commentariorum Mathematicorum Universitatis Sancti Pauli, XXVII, pp.97-100.
  4. Derived rules related to a constructive theory of metric spaces in intuitionistic higher order arithmetic without countable choice, 1980, Annals of Mathematical Logic, 19, pp.33-65
  5. On set theories in toposes, 1981, Logic Symposia, Hakone 1979 -1980, Springer Lecture Notes in Math. 891, Springer-Verlag, Muller, G.H., Takeuti, G., Tugue, T. (eds), pp.23-29
  6. A note on the bar induction rule, 1982, The L.E.J. Brouwer Centenary Symposium, North-Holland, Troelstra, A.S., van Dalen, D. (eds.), pp.149-163
  7. Extracting Lisp programs from constructive proofs: a formal theory of constructive mathematics based on Lisp, 1983, Publications of the Research Institute for Mathematical Sciences, Kyoto University, vol. 19, pp.169-191
  8. 代数仕様とカテゴリー, 1985, コンピュータ・ソフトウェア, vol. 2 pp.30-40
  9. Self-similar sets as Tarski's fixed points, 1985, Publications of the Research Institute for Mathematical Sciences, Kyoto University, 21, pp.1059-1066
  10. Adjunction of semifunctors: categorical structures in non-extensional lambda calculus, 1985, Theoretical Computer Sciences,41, pp.95-104
  11. PX: a system extracting programs from proofs, 1987, Proceedings of the IFIP TC 2/WG 2.2 Working Conference on Formal Description of Programming Concepts, M. Wirsing ed., North-Holland, 3, pp. 99-124
  12. Category theory for algebraic specifications, 1988, vol. 1, Advances in Software Science and Technology, pp. 169-185.
  13. An introduction to PX, 1990, Logical Foundations of Functional Programming, G. Huet ed., Addison-Wesley, pp. 432-486.
  14. Constructive Mathematics and Computer-Aided Reasoning Systems , 1990, MATHEMATICAL LOGIC, P.P. Petkov ed., Plenum Press, pp. 43-52
  15. Lifschit'z Logic of Calculable Numbers and Optimizations in Program Extraction , 1994, Festschrift for Prof. S. Takasu (N. Jones, M. Hagiya and M. Sato eds.), Lecture Notes in Computer Science, Springer, vol. 792, pp. 1-9, S. Hayashi and Y. Takayama
  16. A functional system with transfinitely defined types, 1994, Festschrift for Prof. S. Takasu (N. Jones, M. Hagiya and M. Sato eds. Lecture Notes in Computer Science, Springer, vol. 792, pp. 31-60, M. Yasugi and S. Hayashi
  17. Singleton, Union, and Intersection Types for Program Extraction, , 1994, Information and Computation, vol. 109, pp. 174-210
  18. Interpretations of transfinite recursion and parametric abstraction in type, 1994, in Words, Languages and Combinatorics II, M. Ito and H. Jurgensen, eds. World Scientific Publish. Co., Singapore, pp. 452-464, M. Yasugi and S. Hayashi
  19. Logic of refinement types, 1994, Proceedings of Esprit Basic Research Action, Types for Proofs and Programs workshop, Nijmegen, The Netherlands,Lecture Notes in Computer Science, Springer, vol. 806
  20. 変貌する数学観 -そのとき形式化は?- 科学基礎論研究 Vol. 22, No. 1,1994,pp. 1-6
  21. A New Formalization of Feferman's System of Functions and Classes and its Relation to Frege Structure , International Journal of Foundations of Computer Science, Vol. 6, No. 3, 1995, pp. 187-202, S. Hayashi and S. Kobayashi
  22. Two extensions of PX system (extended abstract), in Linear Logic 96 Tokyo Meeting, Keio University, Tokyo, 1996, in Electronic Notes of Theoretical Computer Science, Vol. 3, http://www.elsevier.nl/mcs/tcs/pc/Menu.html, Elsevier-Science Publishing, S. Hayashi, M. Ishikawa, S. Kobayashi, H. Nakano, S. Nakazaki
  23. Constructive programming - a personal view -, in Combinatorics, Complexity, Logic, Proceedings of DMTCS'96, Springer-Verlag, Singapore, 1996, pp.38-51, D. S. Bridges, C. Calude, J. Gibbons, S. Reeves, I. Witten (eds.)
  24. "山口昌哉「複雑系科学の哲学に不足しているもの」"に対するコメント、日本ファジイ学会誌, 9(5), 611-613, 1997.
  25. Susumu Hayashi, Ryosuke Sumitomo; Testing Proofs by Examples, in Advances in Computing Science, Asian '98 : 4th Asian Computing Science Conference, Manila, the Philippines, December 1998, J. Xiang and Ohori, eds., Lecture notes in Computer Science No. 1538, pp.1-3, 1998.
  26. 証明アニメーション支援環境の構築、コンピュータソフトウェア、Vol.16, No.3 (1999), pp.71-74, 住友亮翼, 林晋
  27. Hayashi S., Sumitomo R., and Shii K.:Towards Animation of Proofs -testing proofs by examples-:, Theoretical Computer Science, 272, pp.177--195, 2002
  28. A limiting first order realizability interpretation, Masahiro Nakata and Susumu Hayashi: Scientificae Mathematicae Japonicae http://www.jams.or.jp/scmjol/5.html, paper number 5-49: dvi, ps, pdf, 2001
  29. Towards Limit Computable Mathematics, Susumu Hayashi and Masahiro Nakata: in Types for Proofs and Programs, International Workshop, TYPES 2000, Durham, UK, December 2000, Selected Paper, P. Challanghan, Z. Luo, J. McKinna, R. Pollack, eds., Springer Lecture Notes in Computer Science 2277, pp.125-144.
  30. Hayashi S.: Mathematics based on Learning, Algorithmic Learning Theory, Lecture Notes in Artificial Intelligence 2533, Springer, pp.7-21.
  31. Akama, Y., Berardi, S., Hayashi, S., Kohlenbach, U.: An Arithmetical Hierarchy of the Law of Excluded Middle and Related Principles. LICS 2004: 192-201
  32. Hayashi, S., Pan Y., Sato M., et al.: Test Driven Development of UML Models with SMART modeling system, in Baars et al. eds.,UML 2004, LNCS. 3273,pp. 395-409, 2004.
  33. Hayashi, S.: Can proofs be animated by gamess?, in P. Urzyczyn ed., TLCA 2005, LNCS 3461, pp.11-22, 2005, invited paper.
  34. Stefano Berardi, Thierry Coquand, Susumu Hayashi: Games with 1-backtracking. GALOP 2005: 210-225
  35. Hayashi, S.:Mathematics based on Incremental Learning -Excluded middle and Inductive inference-, Theoretical Computer Science 350 (1), 2006, pp. 125-139, exteded journal version of 28.
  36. Hayashi, S.: Can proofs be animated by games?, Fundamenta Informaticae 77 (2007), pp.1-13, in print, exteded journal version of 33.
  37. 文献研究と情報技術 : 史学・古典学の現場から(<特集>歴史知識学) , 人工知能学会誌, 25(1), pp.24-31, 2010年1月.
  38. Stefano, Berardi , Thierry, Coquand , Susumu, Hayashi?: Games with 1-backtracking, Annals of Pure and Applied Logic, vol.161-10, July 2010, pp.1254-1269.

商業誌に掲載された解説記事・エッセイなど

  1. 証明とプログラム: 数理科学,特集「応用論理」
  2. 構成的プログラミング: 平成元年, bit, 2月号
  3. 対角線論法とフラクタル: 平成元年, Computer Today, 8月号,特集「これがフラクタルだ」
  4. 計算機と無限: 平成2年, 数学セミナー, 8月号
  5. 証明は死んだ: 平成5年1, 日経サイエンス , 12月号, 共訳 (林・山岸・松木平)
  6. 計算機科学のすすめ:数学セミナー
  7. プリズム通り:三村昌泰,林晋らによるリレー連載,数学セミナー
  8. パズルの論理学: 平成7年, 数理科学, 特集「論理学のおもしろさ」
  9. 圏のファンクション: 平成8年, 数学セミナー 6月号
  10. 数学基礎論三つの神話: 平成11年, 数学セミナー 6月号
  11. 公理主義って知っていますか?: 平成11年,数学セミナー??月号, pp.??-??
  12. 世界をまるごと理解できるだろうか、AERA Mook、「数学がわかる」、pp.30-33, 2000年
  13. モジュール化と科学、岩波書店雑誌「科学」2001年6月号, 特集2あなたが考える科学とは第2回、pp.800-801
  14. ヒルベルトの数学手帳, 数学セミナー, 2007年5月号

最近の査読を経ていない論文と報告等

  1. S. Hayashi, Formalized Mathematics, Proof Animation, and Limit Computable Mathematics, Relevance and Feasibility of Mathematical Analysis on the Computer, RIMS, Kyoto, March 21/22, 数理解析研究所講究録, 2000
  2. 林晋, ヒルベルトと20世紀学数学、雑誌「現代思想」、2000年10月臨時増刊、 総特集=数学の思考, pp.30-41
  3. 林晋、黒川利明, 二つの合理性と日本のソフトウェア工学、 科学技術政策研究所、科学技術動向センター、「科学技術動向」2004年9月号
  4. 林晋、解説「ソフトウェア開発法の新傾向」、応用物理学会、光学、第34巻, 第8号, 2005年8月、 特集「光技術と技術経営:国際競争力回復を目指して」
  5. 林晋, 情報通信技術と「思想」 ―科学技術の能力としての「思想」―、 科学技術政策研究所、科学技術動向センター、「科学技術動向」, 2006年10月号
  6. 林晋、黒川利明、日本の危機としてのIT人材問題科学技術政策研究所、科学技術動向センター、「科学技術動向」2008年7月号
  7. 林晋,「数理哲学」としての種の論理―田辺哲学テキスト生成研究の試み(一)―、京都大学文学部、日本哲学史研究室紀要「日本哲学史研究」, 第7号, 2010年9月.
  8. 林晋,「田辺元の『数理哲学』」、「情報の宝庫 -二つの田辺文庫−」、雑誌「思想」2012年1月号
  9. 林晋,「澤口昭聿・中沢新一の多様体哲学について ―田辺哲学テキスト生成研究の試み(二)―」、京大文日本哲学史専修紀要「日本哲学史研究」、2012年10月 フルバージョンは2013.02.01から公開予定。

主な招待講演等

国際会議・国際ワークショップ(国内含む)

  1. An Introduction to PX: Institute of Logical Foundations of Functional Programming, 1987, Year of Programming, Texas University, Austin, published version.
  2. Constructive Mathematics and Computer-Aided Reasoning Systems: 1988, Heyting '88, Chaika, Bulgaria, published version
  3. Kreisel-Troelstra realizability interpretation and program extraction: 1988, Workshop on Programming Logic, Bastad, Sweden, publisehd version.
  4. ATT: an optimized Curry-Howard isomorphism: 1989, Esprit Basic Research Action, The first Logical Framework Meeting, Sophia-Antipolis, France
  5. Singleton, Union and Intersection Types for Program Extraction : 1991, Theoretical Aspects of Computer Science '91, Sendai, Japan, published version
  6. Representing logic in ATTT: Esprit Basic Research Action, Types for Proofs and Programs workshop, 1993, Nijmegen, The Netherlands, published version.
  7. Feferman's theory and Frege Structure: 1993, The 5th Asian Logic Conference, Singapore, published version
  8. Two Extensions of PX system: 1996, Linear Logic 96, Tokyo Meeting, published version
  9. Constructive programming - a personal view -, DMTCS'96, published version
  10. A series of invited lectures at MSJ Regional Workshop: Theories of Types and Proofs (TTP-Tokyo), Sept. 8-18, 1997,Tokyo Institute of Technology, Tokyo, Japan:
  11. Testing Proofs by Examples, Asian Computing Science Conference '98, Dec. 8-10, 1998, Manila, Philipin, published version.
  12. Limit Computable Mathematics and Proof Animation, TYPES 2000.
  13. S. Hayashi and K. Nakatogawa, Hilbert and Computation, Hilbert Workshop, Jan. 12, 2002, Keio University, Tokyo, organized by Dept. of Philosophy, Keio University, sponsored by Philosophy of Science Society, Japan, and Mita Philosophy Society.
  14. Limit Computable Mathematics and Interactive Computation, The International Workshop on Rewriting in Proof and Computation (RPC'01), October 25-27, 2001, Itutsubashi-kaikan, Sendai, organized by Research Institute of Electrical Communication Tohoku University.
  15. S. Hayashi and Y. Akama, Limit-Computable Mathematics and its Applications, CSL'02 (Computer Science Logic 2002), Edinburgh, UK.
  16. S. Hayashi, Mathematics based on Learning, (Algorithmic Learning Theory 2002), Lubeck, Germany.
  17. 長幼序あり -ソフトウェア工学にみる慣習と技術の問題- “The order of seniority - social traditions and software engineering-” 国際会議
    人口の高齢化に対応した人的資源マネジメントと労働政策 - 日独比較-(ドイツー日本研究所、東京 / ミュンヘン大学日本センター(LMU) , 東京大学大学院工学系研究科 / フリードリヒ・エーベルト財団 共催) における講演およびパネル。2005 三月
  18. S. Hayashi, Can proofs be animated by proofs?, TLCA 05, Nara, Japan, April, 2005.
  19. Proof Animation, Limit Computable Mathematics, and Hilbert’s finite basis theoremMax-Planck-Institut fuer Mathematik, Bonn Conference “Methods of proof theory in mathematics” Hoersaal MPIM, June 2007, 3-10, a talk in an invitation-only conference.
  20. SMART-GS Project: a tool searching, marking up and linking historical documents, 科研費特定領域研究「日本の技術革新−経験蓄積と知識基盤化−」、第3回国際シンポジウム、2007年12月14-15日、東京、第1セッション講演とパネル。

国内会議・ワークショップなど

  1. 構成的数学の諸相:1981,昭和56年度総会数学基礎論分科会特別講演
  2. 計算機科学のための数理論理学: 平成2年, ソフトウェア科学会年会チュートリアル
  3. 論理学と計算機科学:平成2年,日本数学会,平成2年度総会数学基礎論分科 会
  4. 証明工学: 平成5年, 日本応用数理学会, 平成5年度年会特別講演
  5. 数学は完璧か?: 平成6年, 日本数学会, 平成6年度年会市民講座
  6. 変貌する数学観 -そのとき形式化は?-: 平成6年6月, 日本学術会議科学基礎論研究連絡委員会主催, 科学基礎論学会共催, 前原昭二記念シンポジウム「形式化について」, published version
  7. ヒルベルトと20世紀数学:平成11年3月29日、日本数学会、企画特別講演、早稲田大学
  8. ソフトウェア開発の新傾向 ― 象の合理性と猿の合理性 ―, 第52回応用物理学関係連合講演会シンポジウム 「光技術と技術経営 ―国際競争力回復を目指して―」 , 2005年3月、報告とパネル
  9. 真のヒルベルト像をもとめて -ヒルベルト研究の現状-杉浦光夫先生傘寿記念第18回数学史シンポジウム, 津田塾大, 2007, 10/27-10/28、招待講演
  10. 渕一博の思想 −なぜ論理だったのか?−: 渕一博記念コロキウム 『論理と推論技術:四半世紀の展開』、基調講演、 2007年10月20日、慶応大学(三田)
  11. 展示: 林研究室、永井研究室(京大), 寺沢研究室(はこだて未来大学), SMART-GSを使った歴史研究, 2010年3月開催会議「文化とコンピューティング」における展示より。
  12. 2011年度西田・田辺記念講演「種の論理再考」、2011年6月4日
  13. 「社会とソフトウェア:あるソフトウェア工学者の経験」、ソフトウェアプロセス改善カンファレンス2012基調講演、2012.10.10、大阪国際交流センター
  14. 京都現代哲学コロキアム第2回例会ワークショップ「社会媒介(メディア)という視点」、2012.8.25、京大楽友会館  「私の近代化研究と社会メディアという視点
  15. 経済学史学会、ヤングスカラーセミナー:講演資料、講習資料
  16. 「JST さきがけ、知の創生と情報社会、2014年1月領域会議特別講演版 社会とソフトウェア:あるソフトウェア工学者の経験」 関連ブログ投稿
  17. 2014年 社会情報学会(SSI) 学会大会 基調講演「開かれた世界、開かれた心、開かれた社会」