経歴

学歴・職歴

• 昭和47年3月：広島大学附属福山高校卒業
• 昭和47年4月：立教大学理学部数学科入学
• 昭和51年3月：立教大学理学部数学科卒業
• 昭和51年4月：立教大学大学院理学研究科博士課程前期入学
• 昭和53年3月：立教大学大学院理学研究科博士課程前期修了：理学修士
• 昭和53年4月：筑波大学大学院数学研究科編入
• 昭和56年3月：筑波大学大学院数学研究科修了：理学博士
• 昭和56年7月：筑波大学文部技官(数学系準研究員)
• 昭和57年4月：東京都立工科短期大学専任講師
• 昭和59年4月：京都大学数理解析研究所 助手
• 平成元年4月：龍谷大学理工学部数理情報学科 助教授
• 平成4年4月：龍谷大学理工学部数理情報学科 教授
• 平成7年4月：神戸大学工学部知能情報工学科 教授
• 平成7年4月：神戸大学大学院自然科学研究科担当
• 平成16年7月-22年3月：文部科学省科学技術政策研究所科学技術動向研究センター客員研究官併任
• 平成17年4月：京都大学教授大学院文学研究科　教授 （現在にいたる）
• 平成17年4月：神戸大学名誉教授

その他

• 昭和60年7月1日〜8月31日： 米国 スタンフォード大学， 計算機科学科に滞在し研究に従事(学術振興会研究員)
• 昭和62年9月15日〜昭和63年8月31日： 英国 エジンバラ大学， 計算機科学科に滞在し研究に従事(学術振興会研究員)
• 昭和63年2月1日〜4月1日： 米国 スタンフォード大学，計算機科学科に滞在し 研究に従事(客員研究員)
• 昭和63年5月20日〜6月17日： 仏国 INRIA，Sophia-Antipolisに滞在し研究に従事 (客員研究員)
• 平成元年4月1日： スウェーデン・チャールマース工科大学計算機科学科 に滞在し研究に従事(学術振興会研究員)

社会的活動

所属学会

• ACM 会員
• IEEE Computer Society 会員

学術誌編集委員

• 昭和63年6月〜平成6年4月：Journal of Pure and Applied Algebra
• 平成2年3月〜終了（終了年不明）： International Journal of Foundations of Computer Science
• 平成3年7月〜平成19年： Mathematical Structures in Computer Science
• 平成4年〜平成5年： Fundamenta Informatica

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

• 昭和63年： Heyting '88 Meeting, Program Committee Member
• 平成2年： IEEE Logic in Computer Science '90 Meeting (LICS '90), Program Committee Member
• 平成3年〜5年： IEEE Logic in Computer Science Meeting, Organizing Committee Member
• 平成3年： Theoretical Aspects of Computer Software '91 Meeting (TACS '91), Program Committee Member
• 平成5年： IEEE Logic in Computer Science '93 Meeting (TACS '93), Program Committee Member
• 平成6年： Theoretical Aspects of Computer Software '94 Meeting (TACS '94), Program Committee Member
• 平成8年： First Conference of the Centre for Descreate Mathematics and Theoretical Computer Science (DMTCS '96), Program Committee Member
• 平成9年： Theoretical Aspects of Computer Software '97 Meeting (TACS '97), September 1997, Sendai, Japan, Program Committee Member
• 平成9年： First IEEE International Conference on Formal Engineering Methods (ICFEM'97), 12-14 November 1997, Hiroshima, Japan, Program Committee Member
• 平成10年： The Third Fuji International Symposium on Functional and Logic Programming, 2-4 April 1998, Kyoto, Japan, Program Committee Member
• 平成10-11年： The integrated formal methods conference IFM99, York, UK.
• 平成11年： The integrated formal methods conference IFM2000, Schloss Dagstuhl, Germany.
• 以後平成15年まで、IFM のＰＣ を務める
• 平成16年：Program Committee, ICALP '04, Track B, July 12-16, 2004, Turku, Finland
• 平成16年：Program Committee, Asian Computing 04, 2004, Thailand

その他

• 平成20年より：JST, 中島さきがけ「知の創生と情報社会」、アドバイザー
• 平成26年より：JST, 安浦さきがけ「社会と調和した情報基盤技術の構築」、アドバイザー
• 平成27年より：経済産業研究所、人工知能が社会に与えるインパクトの考察：文理連繋の視点から、委員

業績

著書

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. 「お話・数学基礎論」八杉満利子・林晋、平成1４年６月２０日, 講談社
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. プリズム通り：三村昌泰，林晋らによるリレー連載，数学セミナー
   • 1991年6月号：友達の友達の，また，その友達は
   • 1991年9月号：プログラミングは最後の手工業！？
   • 1991年12月号：後向きの考え方
   • 1992年3月号：ワークステーションの買い方
8. パズルの論理学： 平成7年, 数理科学, 特集「論理学のおもしろさ」
9. 圏のファンクション： 平成8年, 数学セミナー 6月号
10. 数学基礎論三つの神話： 平成11年, 数学セミナー 6月号
11. 公理主義って知っていますか？: 平成１１年，数学セミナー??月号, pp.??-??
12. 世界をまるごと理解できるだろうか、AERA Mook、「数学がわかる」、pp.30-33, 2000年
13. モジュール化と科学、岩波書店雑誌「科学」2001年6月号, 特集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世紀学数学、雑誌「現代思想」、２０００年１０月臨時増刊、 総特集＝数学の思考, pp.30-41
3. 林晋、黒川利明, 二つの合理性と日本のソフトウェア工学、　科学技術政策研究所、科学技術動向センター、「科学技術動向」2004年9月号
4. 林晋、解説「ソフトウェア開発法の新傾向」、応用物理学会、光学、第34巻, 第8号, 2005年8月、 特集「光技術と技術経営：国際競争力回復を目指して」
5. 林晋, 情報通信技術と「思想」 ―科学技術の能力としての「思想」―、　科学技術政策研究所、科学技術動向センター、「科学技術動向」, 2006年10月号
6. 林晋、黒川利明、日本の危機としてのＩＴ人材問題、科学技術政策研究所、科学技術動向センター、「科学技術動向」2008年7月号
7. 林晋,「数理哲学」としての種の論理―田辺哲学テキスト生成研究の試み（一）―、京都大学文学部、日本哲学史研究室紀要「日本哲学史研究」, 第７号, 2010年9月.
8. 林晋，「田辺元の『数理哲学』」、「情報の宝庫　-二つの田辺文庫−」、雑誌「思想」２０１２年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:
    • Comparing constructive programming with practical formal methods -Constructive programming is possible but not indispensable-, Sept. 8, 1997
    • Towards Proof Animation from Constructive Programming, Sept. 9, 1997
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 toolsearching, marking up and linking historical documents, 科研費特定領域研究「日本の技術革新−経験蓄積と知識基盤化−」、第3回国際シンポジウム、2007年12月14-15日、東京、第１セッション講演とパネル。

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

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