Vita of Susumu Hayashi

Education

• Department of Mathematics, Rikkyo University, Bachelor of Science, 1976
• Master Course of Mathematics, Graduate School of Rikkyo University, Master of Science, 1978
• Doctor Course of Mathematics, Graduate School of Tsukuba University, Doctor of Science, 1981

Professional experience

• Lecturer of Mathematics, Metropolitan College of Technology, Tokyo, 1982-1984
• Research associate, Research Institute of Mathematical Sciences, Kyoto University, 1984-1989
• Associate professor, Department of Applied Mathematics and Informatics, Ryukoku University, 1989-1992
• Professor, Department of Applied Mathematics and Informatics, Ryukoku University, 1992-1995
• Professor, Department of Computer and Systems Engineering, Kobe University, 1995-2004
• Guest researcher(part time), National Institute of Science and Technology Policy, 2004-present
• Professor, Department of Humanistic Informatics, Graduate School of Letters, Kyoto University, 2005-present

Social activities

• ACM member
• IEEE Computer Society member
• Japanese Society of Software Science and Technology member
• Japanese Society of Mathematics member
• Editorial Board, Journal of Pure and Applied Algebra, 1988-1994
• Editorial Board, International Journal of Foundations of Computer Science, 1990-present
• Editorial Board, Mathematical Structures in Computer Science, 1991-present
• Editorial Board, Fundamenta Informatica, 1992-1996
• Program Committee, Heyting '88 Meeting, 1988
• Program Committee, IEEE Logic in Computer Science '90 Meeting, 1990
• Organizing Committee, IEEE Logic in Computer Science Meeting, 1993-1995
• Program Committee, Theoretical Aspects of Computer Software '91 Meeting, 1991
• Program Committee, IEEE Logic in Computer Science '93 Meeting, 1993
• Program Committee, Theoretical Aspects of Computer Software '94 Meeting, 1994
• Program Committee, Descreate Mathematics and Theoretical Computer Science, 1996
• Program Committee, First IEEE International Conference on Formal Engineering Methods (ICFEM'97) 12-14 November 1997, Hiroshima, Japan
• Program Committee, The Third Fuji International Symposium on Functional and Logic Programming, 2-4 April 1998, Kyoto, Japan
• Program Committee, The integrated formal methods conference IFM1999, 2000, 2002, 2003, 2004
• Program Committee, ICALP '04, Track B, July 12-16, 2004, Turku, Finland
• Program Committee, Asian Computing 04, 2004, Thailand
• NSF reviewer: twice

Books

1. PX: A Computational Logic , S. Hayashi and H. Nakano, 1988, The MIT Press, Now available free.
2. SuriRonriGaku (Mathematical Logic), 1988, Corona-Shya Pub. Co., in Japanese
3. Kouseiteki Puroguramingu no Kiso (The Foundations of Constructive Programming), , 1991, Yusei-Shya Pub. Co., S. Hayashi and S. Kobayashi, in Japanese
4. Jyouhou-kei no Sugaku Nyumon (Introduction to Mathematics for Information Science) , 1993, Ohm-Shya Pub. Co., S. Hayashi and M. Yasugi, in Japanese
5. Geederu no Nazo wo Toku (Unwinding Goedel's Eniguma), 1993, Iwanami-Syoten Pub. Co., in Japanese
6. Puroguramu Kenshyo Ron (Theory of Program Verification), , 1995, Kyoritu-Syuppan Pub. Co., in Japanese
7. Ronri pazuru to pazuru no ronri (Logic puzzles and logic of puzzles), M. Yasugi and S. Hayashi, 1998, Yusei-Shya Pub. Co., in Japanese
8. Paradokusu! (Paradox!), S. Hayashi, ed., Nihon-Hyoron-shya, 2000, in Japanese
9. Ohanasi Sugaku Kisoron M. Yasugi & S. Hayashi, Kodan-shya, 2002, in Japanese
10. Incompleteness theorem, K. Gödel, translated into Japanese and annotated by S. Hayashi and M. Yasugi

Refereed or invited papers

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. Self-similar sets as Tarski's fixed points, 1985, Publications of the Research Institute for Mathematical Sciences, Kyoto University, 21, pp.1059-1066
9. Adjunction of semifunctors: categorical structures in non-extensional lambda calculus, 1985, Theoretical Computer Sciences,41, pp.95-104
10. 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
11. Category theory for algebraic specifications, 1988, vol. 1, Advances in Software Science and Technology, pp. 169-185.
12. An introduction to PX, 1990, Logical Foundations of Functional Programming, G. Huet ed., Addison-Wesley, pp. 432-486, invited paper
13. Constructive Mathematics and Computer-Aided Reasoning Systems , 1990, MATHEMATICAL LOGIC, P.P. Petkov ed., Plenum Press, pp. 43-52 , invited paper
14. 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
15. 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
16. Singleton, Union, and Intersection Types for Program Extraction, , 1994, Information and Computation, vol. 109, pp. 174-210
17. 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
18. 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, invited paper
19. Henbou Suru Sugaku-Kan -Sonotoki Keishikikawa?- (New Trends of Mathematics and their Implications to Formalization), Journal of the Japan Association for Philosophy of Science, Vol. 22, No. 1, 1994, pp. 1-6, in Japanese, invited paper
20. 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
21. 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, invited paper
22. Constructive programming - a personal view -, To appear 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.), invited paper
23. 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 A. Ohori, eds., Lecture notes in Computer Sciences No. 1538, pp.1-3, 1998, invited paper (extended abstract).
24. Susumu Hayashi and Masahiro Nakata: Towards Limit Computable Mathematics,dvi, ps, pdf,in Paul Callaghan and Zhaohui Luo and James McKinna and Robert Pollack, eds., Types for Proofs and Programs, International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000, Selected Papers, Springer Lecture Notes in Computer Science, volume 2277, 2000, pp. 125-144, invited paper.
25. Hayashi S., Sumitomo R., and Shii K.:Towards Animation of Proofs -testing proofs by examples-:, Theor. Comput. Sci.}, volume 272, 2002, pp. 177-195.
26. Masahiro Nakata and Susumu Hayashi: A limiting first order realizability interpretation, dvi, ps, pdf, Scientiae Mathematicae Japonicae Vol. 55, No. 3, pp. 567 - 580.
27. Susumu Hayashi and Masahiro Nakata: Towards Limit Computable Mathematics,dvi, ps, pdf, Theor. Comput. Sci., Vol. 272, 2002, pp. 177-195. (Journal version of the airticle 24.)
28. Hayashi S.: Mathematics based on Learning, Algorithmic Learning Theory, Lecture Notes in Artificial Intelligence 2533, Springer, pp.7-21, 2002.
29. Akama, Y., Berardi, S., Hayashi, S., Kohlenbach, U.: An arithmetical hierarchy of the law of excluded middle and related principles, 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings. IEEE Computer Society 2004, pp.192-201.
30. 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.
31. Hayashi, S.: Can proofs be animated by gamess?, in P. Urzyczyn ed., TLCA 2005, LNCS 3461, pp.11-22, 2005, invited paper.
32. 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.
33. Hayashi, S.: Can proofs be animated by games?, Fundamenta Informaticae 77 (2007), pp.1-13, in print, exteded journal version of 32.

Invited talks at International Conferences and Workshops

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.
12. Proof Animation and Limit Computable Mathematics, TYPES 2000 Annual Meeting, Dec, 2000, Durham, UK, preprint
13. Mathematics Based on Learning., ALT 2002, Lubeck, Germany, November 24 - 26, 2002
14. Can proofs be animated by gamess?, TLCA 05 at Nara, Japan, April 22, 2005