経歴

学歴・職歴

• 昭和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月：文部科学省科学技術政策研究所科学技術動向研究センター客員研究官併任 （現在にいたる）
• 平成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

業績

著書

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日、岩波書店、岩波文庫
    正誤表 （内容に誤りあるいは不適当で修正を行った場合、ここに掲示します。日本語の改善・修正等、文章の内容に関係が薄い修正は掲示しないこともあります。）
    • 第2刷で行った修正： p.191上から14行目, p.276下から2行目 の「ベリー」は「リシャール」の間違い。（p.191上から1行目の「ベリー」は正しい。）リシャールに修正し、それに関連してpp.190-191の文章を修正。
    • 第3刷で行った修正：p.233の脚注106。「後の講義録を読んだだけの可能性も高いようだ」を「後に講演の内容を知っただけの可能性もあるようだ」に修正。(出典は J. Dawson, Logical Dilemmas)
    • 第４刷で行った修正：
      • p.98 上から７行目：「Modultheorie」を「Modulsystem の理論」に訂正。Kronecker 自身はModulsystem という名で、Modul の理論の代数を呼び、Modultheorie という呼び名は使っていない。また、Modultheorie では現代のモジュール理論と混同してしまうことからも不適当。
      • p.144下から６行目から５行目の「繰り返し使われていた」は「本質的に使われていた」に訂正。
      • p.228上から４行目から５行目「児童の心理発達の数学理論で有名になるピアジェ」は「数学における発見法の著作で有名になるP\'olya」に訂正。
      • p.89第２パラグラフ。コーシーが「連続ならば微分可能」という「定理」の証明を何度も試みては失敗したという記述は根拠がない。おそらく間違っている。１９世紀解析学史研究者の中根美知代さんの御指摘です。
      • p.120以後に「イグノラミブス」および "ignoramibus" というラテン語のカナ表記とラテン語が多数あるが、「イグノラビムス」 と "ignorabimus" の間違い。
        • 福岡大学人文学部の上枝美典さん（中世哲学）に御指摘いただきました。脱稿直前に、ラテン語のスペルを間違えていた個所に引きづられ、正しい表記を間違えた表記に　emacs のコマンドを使って一括で書き換えてしまった記憶があります。今まで見つかった内の最大のポカミスです。現在までにこの誤りが見つかっているページ： pp.120, 121, 139, 152, 156, 214, 246
      • p.152の「ノスセムス」を「ノスケムス」に変更。ラテン語は発音の方式が何通りかあるが、現在のものは「イギリス系」。これを上枝美典さんに教えていただき、古典ラテン語の発音に統一することにした。上枝さんの御意見では、「ノスケームス」の方が良く、同様に、「イグノラービムス」の方がよい。しかし、「習慣」に従い「イグノラビムス」とし、それに合わせて「ノスケムス」とした。
      • p.229の下から２行目からp.230の上から４行目「PRA に…この証明は正しかった.」を次のように変更「PRA の第２階算術版から帰納法を除いたものなどの、様々な形式系を考え、 それらの無矛盾性証明を実行し易い「小さい」システムから順番に実行すると いう方針をとった. それらは数学的に言えば PRA とその様々な拡張の無矛盾性証明になっていた. 」； p.230上から５行目「という」を「などの」に変更。；p.230 上から12行目「ようやくその本質的問題点を理解したのである.」を「それが意図した有限の立場を超えていることを理解したのだろう.」に変更。
        • 中部大学の渕野昌さんからp.230にある Ackermann の論文についての記述で私が PRA と書いているところが、実際の Ackermann の論文では第２階の算術になっていると指摘されました。この部分は文献[17]の Zach さんの論文を元に書いたところですが、確認しましたら Zach さんの論文を読み違えていました。上の３箇所の修正の内、第１,２の修正で Zach さんの論文の内容に合うようになります。第３の修正は文章の意味を明瞭にするための改善です。
    • 第5刷で行った修正：
      • p.228上から４行目の人名 Polya の表記が間違って数式のようになっています。Polya はハンガリー人で、正しい表記は、こちらのようになります。林、岩波文庫編集部、印刷会社の３者の意思疎通が、どこかで乱れてしまった。
      • p.94上から９行目：１８９４年は１８７４年に訂正。
      • p.243上から4行目から：「彼は, アッカーマンが第1階算術の無矛盾性を証明したというヒルベルトの主張を信じた. そして, それならば, 第2階算術の解釈を, 第1階算術を使って作れば十分」を、「彼は, アッカーマンやヒルベルトが主張したように第1階算術の無矛盾性を証明できるというのならば, 第2階算術の解釈を第1階算術を使って作れば十分」に変更。 これは Hao Wang のレポートによるが, それではゲーデルが第1階の無矛盾性証明ができたと信じていたという確実な証拠にはならない。
      • p.246上から6行目：「フォン・ノイマンの示唆であるという説もある. つまり, ケーニヒスベルグの発言の時点でゲーデルが得ていたのは第2節の結果までだという説である.」を 「フォン・ノイマンの示唆であるという. つまり, ケーニヒスベルグの発言の時点でゲーデルが得ていたのは論文第2節までの結果だと思われる.」に変更。同10行目：「詳細は」を「詳細までは」に変更。
      • p.141上から13行目：「四則演算だけで」を 「和と積の二演算だけで」に訂正。
      • p.163 下から下から9行目「ヒルベルトの方法の信奉者に変わっていた．」を「ヒルベルトの方法を認めるようになっていた．」
    • 第6刷で行った修正（これを書いている2009年9月初旬では6刷はまだ印刷の準備中）：
      • 最初にコメントです。今回は初めて訳文の方に修正がかなりでました。すべて野村光義さんの指摘です。丁寧にチェックしてもらったことを感謝します。表現の変更などはここでは掲示しない原則ですが、数式のコンマの区切り位置などの修正が内容の修正か文言の修正かは判断が分かれます。数学の場合は表現上の変更でも掲示した方が学生さんなどには良いだろうと思いますので、今回は原則を緩めてできるだけ沢山掲示しました。以下、殆どは野村さんからのメールから直接取っています。
    • p.29の IVに２箇所、フォントの間違いがある。R(x,y) の２箇所のFraktur(独逸文字）の xはイタリック（変数）の小文字のxに訂正。
      
    • p.30の脚注32：「定義から」→「αの定義から」
    • p. 12, 一番下の行： 「ボールド体」→「スモール・キャピタル」
    • p. 37の定義33： 「n番目の【型持ち上げ】」→「【n番目の型持ち上げ】」
    • p. 44, 原注43，最後の行： 「置き換えて」→「【置き換えて】」
    • p. 46, 10行目： 【n-項関係記号】→ n-項【関係記号】
    • p. 47, 下から8行目： 【κ-証明可能】→κ-【証明可能】
    • p. 55, 下から5行目： 「PM, I, 14」→「PM, I, *14」
    • p. 56の1, 2, 3 の各1行目の限量記号内： 「(x2…xm)」→「(x2, …, xm)」と「(x1…xm)」→「(x1, …, xm)」
    • p. 59, 下から4-5行目： 「第１節，p. 44」→「p. 44の1」
    • p. 67など 訳注に数箇所：「Heijernoort」→「Heijenoort」
    • p. 276 冒頭：「この章では…数学的・論理学的仕組みを説明し，また……論文の仕組 みを詳しく説明する」→「この章では…説明し，また次の第8章では……説明する」
      
      

主な学術論文（査読論文・招待論文）

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.
    

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

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月号
   

主な招待講演等

国際会議・国際ワークショップにおける招待講演・基調講演・パネル等

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日、慶応大学（三田）