Masami Hagiya

Masami Hagiya is a professor at
Department of Computer Science,
Graduate School of Information
Science and Technology,
University of Tokyo.

He is in Rooms 203 and 211,
Science Building No.7,
Department of Computer Science,
Graduate School of Information
Science and Technology,
University of Tokyo,
7-3-1 Hongo, Bunkyo-ku,
Tokyo 113-8656, JAPAN.

TEL: +81-3-5841-4113 (PHS)
TEL: +81-3-5841-4093 (laboratory)
FAX: +81-3-5841-0762
E-mail: hagiya at is.s.u-tokyo.ac.jp
Twitter: at hagiya (mostly in Japanese)

[pics]
by Yohei Hagiya


Links


Introduction

Masami Hagiya is a professor at Department of Computer Science, University of Tokyo. After receiving M.Sc. from University of Tokyo, he worked for Research Institute for Mathematical Sciences, Kyoto University, and received Dr.Sc. He has been working on modeling, formalization, simulation, verification, and automatic synthesis of computer systems, mainly using deductive approaches. He is not only dealing with systems composed of electronic computers, but also with biological and molecular systems, and has been working on DNA and molecular computing. Finally, he is also interested in how those systems are evolved, either by human intelligence or by artificial intelligence.

Introduction to Hagiya Laboratory

With background in formal logic, our laboratory is seeking for new computational models and developing methods and tools for their analysis, verification and synthesis. While our laboratory has been working on formal verification of software and protocol, we are now mainly investigating potential of computation not by conventional electronic computers but by natural phenomena including physical, chemical and biological ones (natural computation or unconventional computation), and conducting research on molecular computing, quantum computing, cellular computing, etc., and their applications (e.g., molecular computing to molecular robotics).

Recent research projects by students:


Publications

Publish and perish!

Refereed Papers (including Conference Papers)

  1. Richard Potter, Cyrille Artho, Kuniyasu Suzaki, and Masami Hagiya: A Knoppix-based demonstration environment for JPF, ACM SIGSOFT Software Engineering Notes, Vol.39 No.1, 2014 pp.1-5.

  2. Nathanael Aubert, Clement Mosca, Teruo Fujii, Masami Hagiya, and Yannick Rondelez: Computer Assisted Design for Scaling Up Systems based on DNA Reaction Networks, Journal of the Royal Society Interface, Vol.11, 20131167, 2014.
  3. * Watcharin Leungwattanakit, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto, and Koichi Takahashi: Modular Software Model Checking for Distributed Systems, IEEE Transactions on Software Engineering, to appear.
  4. Nathanael Aubert, Yannick Rondelez, Teruo Fujii, and Masami Hagiya: Enforcing delays in DNA computing systems, Natural Computing, to appear.
  5. Cyrille Artho, Masami Hagiya, Richard Potter, Yoshinori Tanabe, Franz Weitl, and Mitsuharu Yamamoto: Software Model Checking for Distributed Systems with Selector-Based, Non-blocking Communication, 28th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2013, pp.169-179.

  6. Cyrille Valentin Artho, Armin Biere, Masami Hagiya, Eric Platon, Martina Seidl, Yoshinori Tanabe, and Mitsuharu Yamamoto: Modbat: A Model-Based API Tester for Event-Driven Systems. Proceedings of the 9th Haifa Verification Conference, Lecture Notes in Computer Science, Vol.8244, 2013, pp.112-128.

  7. Nathanael Aubert, Quang Huy Dinh, Masami Hagiya, Teruo Fujii, Hitoshi Iba, Nicolas Bredeche, and Yannick Rondelez: Evolving cheating DNA networks: a Case Study with the Rock-Paper-Scissors Game, ECAL, 2013, pp.1143-1150
  8. * Masami Hagiya and Ibuki Kawamata: Towards Co-evolution of Information, Life and Artificial Life, Natural Computing and Beyond, Proceedings in Information and Communications Technology, Vol.6, 2013, pp.39-48.
  9. Ibuki Kawamata, Nathanael Aubert, Masahiro Hamano and Masami Hagiya: Abstraction of Graph-Based Models of Bio-Molecular Reaction Systems for Efficient Simulation, Computational Methods in Systems Biology, 10th International Conference, CMSB 2012, Lecture Notes in Bioinformatics, Vol.7605, 2012, pp.187-206.

  10. Miki Hirabayashi, Ibuki Kawamata, Masami Hagiya, Hiroaki Kojima, and Kazuhiro Oiwa: In Silico Design Control of the Trade-Off Balance in Robustness and Fragility of Logical Circuits Using DNA Nanostructures, IEEE NANO 2012, 2012, pp.1-6.
  11. * Hubert Comon-Lundh, Masami Hagiya, Yusuke Kawamoto, and Hideki Sakurada: Computational soundness of indistinguishability properties without computable parsing, The 8th International Conference on Information Security Practice and Experience (ISPEC 2012), Lecture Notes in Computer Science, Vol.7232, 2012, pp.63-79.

  12. Ryoji Sekine, Masayuki Yamamura, Shotaro Ayukawa, Kana Ishimatsu, Satoru Akama, Masahiro Takinoue, Masami Hagiya, and Daisuke Kiga: Tunable synthetic phenotypic diversification on Waddington's landscape through autonomous signaling, Proceedings of the National Academy of Sciences of the United States of America, Vol.108, 2011, pp.17969-17973.
  13. * Watcharin Leungwattanakit, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, and Mitsuharu Yamamoto: Model Checking Distributed Systems by Combining Caching and Process Checkpointing, 26th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2011, pp.103-112.

  14. Miki Hirabayashi, Akio Nishikawa, Fumiaki Tanaka, Masami Hagiya, Hiroaki Kojima, and Kazuhiro Oiwa: Design of Molecular-Based Network Robots - Toward the Environmental Control, IEEE NANO 2011, 2011, pp.313-318.
  15. Kosuke Ono, Yoichi Hirai, Masami Hagiya and Yoshinori Tanabe: Using Coq in Specification and Program Extraction of Hadoop MapReduce Applications, 9th International Conference on Software Engineering and Formal Methods (SEFM 2011), Lecture Notes in Computer Science, Vol.7041, 2011, pp.350-365.

  16. Ibuki Kawamata, Fumiaki Tanaka, and Masami Hagiya: Abstraction of DNA Graph Structures for Efficient Enumeration and Simulation, The 2011 International Conference on Parallel and Distributed Processing, Techniques and Applications (PDPTA'11), Technical Session on Mathematical Modeling and Problem Solving, 2011, pp.800-806.

  17. Fumiaki Tanaka, Toshio Mochizuki, Xingguo Liang, Hiroyuki Asanuma, Shukichi Tanaka, Katsuyuki Suzuki, Shin'ichi Kitamura, Akio Nishikawa, Kumiko Ui-Tei, and Masami Hagiya: Robust and photo-controllable DNA capsules using azobenzenes, Nano Letters, Vol.10, No.9, 2010, pp.3560-3565.
  18. Miki Hirabayashi, Akio Nishikawa, Fumiaki Tanaka, Masami Hagiya, Hiroaki Kojima, and Kazuhiro Oiwa: DNA-based Crosstalk Nanorobot Mimicking Amoeba Type of Slime Funguses, IEEE NANO 2010, 2010, pp.864-869.
  19. Cyrille Artho, Watcharin Leungwattanakit, Masami Hagiya, Yoshinori Tanabe, and Mitsuharu Yamamoto: Model Checking of Concurrent Algorithms: From Java to C, DIPES 2010, 7th IFIP Conference on Distributed and Parallel Embedded Systems, IFIP AICT, Vol.329, 2010, pp.90-101.

  20. Alexis Goyet, Masami Hagiya and Yoshinori Tanabe: Decidability and undecidability results on the modal mu-calculus with a natural number-valued semantics, Logic, Language, Information and Computation, 17th International Workshop, WoLLIC 2010, Lecture Notes in Artificial Intelligence, Vol.6188, 2010, pp.148-160.

  21. Yoshinori Tanabe and Masami Hagiya: Fixed-point Computations over Functions on Integers with Operations Min, Max and Plus, 6th Workshop on Fixed Points in Computer Science (FICS 2009), Coimbra, Portugal, 12-13 September 2009, pp.108-115.

  22. Miki Hirabayashi, Kazuhiro Oiwa, Akio Nishikawa, Fumiaki Tanaka, and Masami Hagiya: Toward Self-Assembly of Phage-Like Nanorobot, IEEE NANO 2009, 2009, pp.645-650.
  23. Cyrille Artho, Watcharin Leungwattanakit, Masami Hagiya, Yoshinori Tanabe and Mitsuharu Yamamoto: Cache-based Model Checking of Networked Applications: From Linear to Branching Time, 24th IEEE/ACM International Conference on Automated Software Engineering, 2009, pp.447-458.

  24. * Ibuki Kawamata, Fumiaki Tanaka, and Masami Hagiya: Automatic Design of DNA Logic Gates Based on Kinetic Simulation, The 15th International Meeting on DNA Computing and Molecular Programming, DNA15, Preliminary Proceedings, 2009, pp.8-17. Also in DNA Computing and Molecular Programming: 15th International Conference, DNA 15, Lecture Notes in Computer Science, Vol.5877, 2009, pp.88-96.
  25. Watcharin Leungwattanakit, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, and Mitsuharu Yamamoto: Verifying networked programs using a model checker extension, ICSE Companion Proceedings, 2009, pp.409-410.

  26. Watcharin Leungwattanakit, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, and Mitsuharu Yamamoto: Introduction of virtualization technology to multi-process model checking, First NASA Formal Methods Symposium, NASA Conference Publication, 2009, pp.106-110.

  27. Yusuke Kawamoto, Hideki Sakurada, and Masami Hagiya: Computationally sound formalization of rerandomizable RCCA secure encryption, Third Franco-Japanese Computer Security Workshop, Nancy, France, March 2008. In Formal to Practical Security, Papers Issued from the 2005-2008 French-Japanese Collaboration, Lecture Notes in Computer Science, Vol.5458, 2009, pp.158-180.

  28. Yoshinori Tanabe, Koichi Takahashi, and Masami Hagiya: A decision procedure for alternation-free modal $\mu$-calculi, Advances in Modal Logic, Vol.7, (C. Areces, R. Goldblatt, Eds.), College Publications, London, 2008, pp.341-362.

  29. * Yusuke Kawamoto, Hideki Sakurada and Masami Hagiya: Computationally Sound Symbolic Anonymity of a Ring Signature, FCS-ARSPA-WITS'08, Joint Workshop on Foundations of Computer Security, Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security, 2008.

  30. Fumiaki Tanaka, Takashi Tsuda, and Masami Hagiya: Towards DNA Comparator: the Machine That Compares DNA Concentrations, The 14th International Meeting on DNA Computing, DNA14, Preliminary Proceedings, 2008, pp.100-111. Also in DNA Computing: 14th International Meeting on DNA Computing, DNA 14, Lecture Notes in Computer Science, Vol.5347, 2009, pp.11-20.
  31. * Cyrille Artho, Watcharin Leungwattanakit, Masami Hagiya and Yoshinori Tanabe: Efficient Model Checking of Networked Applications, TOOLS-EUROPE 2008, Lecture Notes in Business Information Processing, Vol.11, 2008, pp.22-40.

  32. Dai Ikarashi, Yoshinori Tanabe, Koki Nishizawa, and Masami Hagiya: Modal $\mu$-calculus on min-plus algebra N$_\infty$, The Tenth Workshop on Programming and Programming Languages (PPL2008), Japanese Society on Software Science and Technology, 2008, pp.216-230. (Awarded Rombun-Shourei-Sho) The full version is in Computer Software, Japanese Society on Software Science and Technology, Vol.27, No.3, 2010, pp.99-113

  33. S. Ayukawa, A. Kobayashi, Y. Nakashima, H. Takagi, S. Hamada, M. Uchiyama, K. Yugi, S. Murata, Y. Sakakibara, M. Hagiya, M. Yamamura and D. Kiga: SYANAC: SYnthetic biological Automaton for Noughts And Crosses, IET Synthetic Biology, Vol.1, No.1-2, 2007, pp.64-67.
  34. Akio Nishikawa, Satsuki Yaegashi, Kazumasa Ohtake, and Masami Hagiya: Multi-fueled Approach to DNA Nano-robotics, The Thirteen International Meeting on DNA Computing, DNA13, Preliminary Proceedings, 2007, pp.162-171. Also in DNA Computing: 13th International Meeting on DNA Computing, DNA13, Lecture Notes in Computer Science, Vol.4848, 2008, pp.79-88. Also in Natural Computing, Vol.7, No.3, 2008, pp.371-383 (online version).
  35. Atsushi Kameda, Satoshi Kashiwamura, Masahito Yamamoto, Azuma Ohuchi, and Masami Hagiya: Combining randomness and a high-capacity DNA memory, The Thirteen International Meeting on DNA Computing, DNA13, Preliminary Proceedings, 2007, pp.261-269. Also in DNA Computing: 13th International Meeting on DNA Computing, DNA13, Lecture Notes in Computer Science, Vol.4848, 2008, pp.109-118.
  36. Carl Christian Frederiksen and Masami Hagiya: Sub-Computation Based Transition Predicate Abstraction, IPSJ Transactions on Programming, Vol.48, No.SIG10(PRO33), 2007, pp.114-137. Also in IPSJ Digital Courier, Vol.3, 2007, pp.380-403.

  37. John A. Rose, Russell J. Deaton, Masami Hagiya, and Akira Suyama: Coupled Equilibrium Model of Hybridization Error for the DNA Microarray and Tag-Antitag Systems, IEEE Transactions on Nanobioscience, Vol.6, No.1, 2007, pp.18-27.
  38. Atsushi Kemada, Masahito Yamamoto, Azuma Ohuchi, Satsuki Yaegashi, and Masami Hagiya: Unravel Four Hairpins!, The Twelfth International Meeting on DNA Computing, DNA12, Preliminary Proceedings, 2006, pp.65-74. Also in DNA Computing: 12th International Meeting on DNA Computing, DNA12, Lecture Notes in Computer Science, Vol.4287, 2007, pp.381-392. Also in Natural Computing, Vol.7, No.2, 2008, pp.287-298 (online version).
  39. Ken Komiya, Satsuki Yaegashi, Masami Hagiya, Akira Suyama, and John A. Rose: Experimental Validation of the Statistical Thermodynamic Model for Prediction of the Behavior of Autonomous Molecular Computers Based on Hairpin Formation, The Twelfth International Meeting on DNA Computing, DNA12, Preliminary Proceedings, 2006, pp.382-392. Also in DNA Computing: 12th International Meeting on DNA Computing, DNA12, Lecture Notes in Computer Science, Vol.4287, 2007, pp.428-438.
  40. John A. Rose, Ken Komiya, Satsuki Yaegashi, and Masami Hagiya: Displacement Whiplash PCR: Optimized architecture and experimental validation, The Twelfth International Meeting on DNA Computing, DNA12, Preliminary Proceedings, 2006, pp.393-403. Also in DNA Computing: 12th International Meeting on DNA Computing, DNA12, Lecture Notes in Computer Science, Vol.4287, 2007, pp.393-403.
  41. Ken Komiya, Kensaku Sakamoto, Atsushi Kameda, Masahito Yamamoto, Azuma Ohuchi, Daisuke Kiga, Shigeyuki Yokoyama and Masami Hagiya: DNA polymerase programmed with a hairpin DNA incorporates a multiple-instruction architecture into molecular computing, BioSystems, Vol.83, No.1, 2006, pp.18-25.
  42. Seika Abe, Masami Hagiya and Ikuo Nakata: A Retargetable Code Generator for the Generic Intermediate Language in COINS, IPSJ Transactions on Programming, Vol.46, No.SIG14(PRO27), 2005, pp.12-29.

  43. Yoshinori Tanabe, Koichi Takahashi, Mitsuharu Yamamoto, Akihiko Tozawa, and Masami Hagiya: A Decision Procedure for the Alternation-free Two-way Modal mu-calculus, TABLEAUX 2005, Lecture Notes in Artificial Intelligence, Vol.3702, 2005, pp.277-291.

  44. Masami Hagiya: Discrete State Transition Systems on Continuous Space-Time: A Theoretical Model for Amorphous Computing, UC 2005, Unconventional Computation, Lecture Notes in Computer Science, Vol.3699, 2005, pp.117-129.

  45. Atsushi Kameda, Masahito Yamamoto, Hiroki Uejima, Masami Hagiya, Kensaku Sakamoto and Azuma Ohuchi: Hairpin-based state machine and conformational addressing: Design and experiment, Natural Computing, Vol.4, No.2, 2005, pp.103-126.
  46. Keiichiro Takahashi, Satsuki Yaegashi, Hiroyuki Asanuma and Masami Hagiya: Photo- and Thermoregulation of DNA Nanomachines, DNA11, Eleventh International Meeting on DNA Based Computers, Preliminary Proceedings, 2005, pp.147-156. Also in DNA Computing: 11th International Workshop on DNA Computing, DNA11, Lecture Notes in Computer Science, Vol.3892, 2006, pp.336-346.
  47. Keiichiro Takahashi, Satsuki Yaegashi, Atsushi Kameda and Masami Hagiya: Chain Reaction Systems Based on Loop Dissociation of DNA, DNA11, Eleventh International Meeting on DNA Based Computers, Preliminary Proceedings, 2005, pp.343-353. Also in DNA Computing: 11th International Workshop on DNA Computing, DNA11, Lecture Notes in Computer Science, Vol.3892, 2006, pp.347-358.
  48. * Yoshihito Nakagawa, Richard Potter, Mitsuharu Yamamoto, Masami Hagiya, and Kazuhiko Kato: Model Checking of Multi-Process Applications Using SBUML and GDB, Workshop on Dependable Software -- Tools and Methods --, Supplemented Volume of the 2005 International Conference on Dependable Systems and Networks, 2005, pp.215-220.

  49. * Osamu Sato, Richard Potter, Mitsuharu Yamamoto and Masami Hagiya: UML Scrapbook and Realization of Snapshot Programming Environment, Software Security -- Theories and Systems, Second Mext-NSF-JSPS International Symposium, ISSS 2003, Tokyo Japan, November 2003, Revised papers, Lecture Notes in Computer Science, Vol.3233, 2004, pp.281-295.

  50. Mitsuhiro Kubota and Masami Hagiya: Minimum Basin Algorithm: An Effective Analysis Technique for DNA Energy Landscapes, DNA10, Tenth International Meeting on DNA Based Computers, Preliminary Proceedings, 2004, pp.202-213. Also in DNA Computing: 10th International Workshop on DNA Computing, DNA10, Lecture Notes in Computer Science, Vol.3384, 2005, pp.202-214.
  51. Mitsuhiro Kubota, Kazumasa Ohtake, Ken Komiya, Kensaku Sakamoto and Masami Hagiya: Branching DNA Machines Based on Transitions of Hairpin Structures, Proceedings of the 2003 Congress on Evolutionary Computation (CEC'03), 2003, pp.2542-2548.
  52. John A. Rose, Masami Hagiya and Akira Suyama: The Fidelity of the Tag-Antitag System 2: Reconciliation with the Stringency Picture, Proceedings of the 2003 Congress on Evolutionary Computation (CEC'03), 2003, pp.2740-2747.
  53. Akihiko Tozawa and Masami Hagiya: XML Schema Containment Checking based on Semi-implicit Techniques, Implementation and Application of Automata, 8th International Conference, CIAA 2003, Lecture Notes in Computer Science, Vol.2759, 2003, pp.213-225.

  54. Hiroki Uejima and Masami Hagiya: Secondary Structure Design of Multi-state DNA Machines Based on Sequential Structure Transitions, DNA9, Ninth International Meeting on DNA Based Computers, Preliminary Proceedings, 2003, pp.80-91. Also in DNA Computing, 9th International Workshop on DNA-Based Computers, DNA9, Madison, WI, USA, June 2003, Revised Papers, Lecture Notes in Computer Science, Springer, Vol.2943, 2004, pp.74-85.
  55. * Masami Haigya, Ryo Takemura, Koichi Takahashi, and Takamichi Saito: Verification of Authentication Protocols Based on the Binding Relation, Software Security -- Theories and Systems, Mext-NSF-JSPS Internationa Symposium, ISSS 2002, Tokyo, Japan, November 2002, Revised papers, Lecture Notes in Computer Science, Springer, Vol.2609, 2003, pp.299-316.

  56. * Mitsuharu Yamamoto, Jean-Marie Cottin, and Masami Hagiya: Decidability of Safety Properties of Timed Multiset Rewriting, FTRTFT'02, Formal Techniques in Real-Time and Fault Tolerant Systems, 7th International Symposium, FTRTFT 2002, Co-sponsored by IFIP WG 2.2, Oldenburg, Germany, September 2002, Proceedings, Lecture Notes in Computer Science, Springer, Vol.2469, 2002, pp.165-183.

  57. Richard Potter and Masami Hagiya: Computation Scrapbooks for Software Evolution, Fifth International Workshop on Principles of Software Evolution, IWPSE 2002, Orlando, Florida, USA, May 19-20, 2002, pp.143-147.

  58. * Koichi Takahashi and Masami Hagiya: Formal Proof of Abstract Model Checking of Concurrent Garbage Collection, Workshop on Thirty Five years of Automath, Informal Proceedings (Fairouz Kamareddine Ed.), Heriot-Watt University, Edinburgh, April, 2002, pp.115-126.

  59. * Koichi Takahashi and Masami Hagiya: Searching for Mutual Exclusion Algorithms Using BDDs, Progress in Discovery Science, (Setsuo Arikawa and Ayumi Shinohara Eds.), Lecture Notes in Artificial Intelligence, Vol.2281, 2002, pp.1-18.

  60. * Akihiko Tozawa and Masami Hagiya: Formalization and Analysis of Class Loading in Java, Higher-Order and Symbolic Computation, Vol.15, 2002, pp.7-55.

  61. J. A. Rose, R.J. Deaton, M. Hagiya, A. Suyama: An Equilibrium Analysis of the Efficiency of an Autonomous Molecular Computer, Physical Review E, Vol.65, No.2-1, 2002, 021910, pp.1-13.
  62. Hiroki Uejima, Masami Hagiya and Satoshi Kobayashi: Horn Clause Computation by Self-Assembly of DNA Molecules, DNA7, 7th International Meeting on DNA Based Computers, Preliminary Proceedings, 2001, pp.63-74. Also in DNA Computing, 7th International Workshop on DNA-Based Computers, DNA7, Tampa, FL, USA, June 2001, Revised Papers, Lecture Notes in Computer Science, Springer, Vol.2340, 2002, pp.308-320.
  63. John A. Rose, Russell J. Deaton, Masami Hagiya, and Akira Suyama: The Fidelity of the Tag-Antitag System, DNA7, 7th International Meeting on DNA Based Computers, Preliminary Proceedings, 2001, pp.302-310. Also in DNA Computing, 7th International Workshop on DNA-Based Computers, DNA7, Tampa, FL, USA, June 2001, Revised Papers, Lecture Notes in Computer Science, Springer, Vol.2340, 2002, pp.138-149.
  64. John. A. Rose, Russell J. Deaton, Masami Hagiya, and Akira Suyama: PNA-mediated Whiplash PCR, DNA7, 7th International Meeting on DNA Based Computers, Preliminary Proceedings, 2001, pp.311-320. Also in DNA Computing, 7th International Workshop on DNA-Based Computers, DNA7, Tampa, FL, USA, June 2001, Revised Papers, Lecture Notes in Computer Science, Springer, Vol.2340, 2002, pp.104-116.
  65. Akio Nishikawa, Masayuki Yamamura and Masami Hagiya: DNA Computation Simulator Based on Abstract Bases, Soft Computing, Vol.5, No.1, 2001, pp.25-38.
  66. Jianguo Lu, John Mylopoulos, Masateru Harao and Masami Hagiya: Higher-order generalization and its application in program verification, Annals of Mathematics and Artificial Intelligence, Vol.28, 2000, pp.107-126.

  67. Kensaku Sakamoto, Hidetaka Gouzu, Ken komiya, Daisuke Kiga, Shigeyuki Yokoyama, Takashi Yokomori and Masami Hagiya: Molecular Computation by DNA Hairpin Formation, Science, Vol.288, 2000, pp.1223-1226.
  68. Masanori Arita, Akio Nishikawa, Masami Hagiya, Ken Komiya, Hidetaka Gouzu and Kensaku Sakamoto: Improving Sequence Design for DNA Computing, Proceedings of the Gnenetic and Evolutionary Computation Conference (GECCO 2000), 2000, pp.875-882.
  69. Ken Komiya, Kensaku Sakamoto, Hidetaka Gouzu, Shigeyuki Yokoyama, Masanori Arita, Akio Nishikawa and Masami Hagiya: Successive State Transitions with I/O Interface by Molecules, DNA6, Sixth International Meeting on DNA Based Computers, Preliminary Proceedings, 2000, pp.21-30. Also in DNA Computing, 6th International Workshop on DNA-Based Computers, DNA 2000, (Anne Condon and Grzegorz Rozenberg Eds.), Lecture Notes in Computer Science, Vol.2054, 2001, pp.17-26.
  70. Akio Nishikawa and Masami Hagiya: Towards a System for Simulationg DNA Computing with Whiplash PCR, CEC'99, Congress on Evolutionary Computation, 1999, pp.960-966.
  71. Akio Nishikawa, Masami Hagiya and Masayuki Yamamura: Virtual DNA Simulator and Protocol Design by GA, Proceedings of the Genetic and Evolutionary Computation Conference, GECCO'99, Vol.2, 1999, pp.1810-1816.
  72. * Mitsuharu Yamamoto and Masami Hagiya: Evolution of Inductive Definitions, IWPSE99, International Workshop on Principles of Software Evolution, Fukuoka Software Research Park, 1999, pp.17-21.

  73. * Akihiko Tozawa and Masami Hagiya: Careful Analysis of Type Spoofing, JIT'99 Java-Informations-Tage 1999 (Clemens H. Cap, Hrsg.), Informatik aktuell, Springer, 1999, pp.290-296.

  74. Jianguo Lu, Masateru Harao and Masami Hagiya: Higher Order Generalizaion, Logics in Artificial Intelligence JELIA'98 (Jurgen Dix, Luis Farinas del Cerro and Ulrich Furback, eds.), Lecture Notes in Artificial Intelligence, Springer-Verlag, Vol.1489, 1998, pp.368-381.

  75. * Masami Hagiya and Akihiko Tozawa: On a New Method for Dataflow Analysis of Java Virtual Machine Subroutines, Static Analysis, 5th International Symposium, SAS'98, Pisa, Italy, September 1998, Proceedings (Giorgio Levi, ed.), Lecture Notes in Computer Science, Springer-Verlag, Vol.1503, 1998, pp.17-32.

  76. * Koichi Takahashi and Masami Hagiya: Proving as Editing HOL Tactics, Informal proceedings of the Workshop on User Interfaces for Theorem Provers, UITP'98 (Roland Backhouse, ed.), Eindhoven University of Technology, 1998, pp.157-164. Also in Formal Aspects of Computing, Vol.11, No.3, 1999, pp.343-357.

  77. * Mitsuharu Yamamoto, Koichi Takahashi, Masami Hagiya, Shin-ya Nishizaki and Tetsuo Tamai: Formalization of Graph Search Algorithms and Its Applications, Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs'98, Canberra, Australia, September/October 1998, Proceedings (Jim Grundy, Malcolm Newey, eds.) Lecture Notes in Computer Science, Springer-Verlag, Vol.1479, 1998, pp.479-496.

  78. Kensaku Sakamoto, Daisuke Kiga, Ken Komiya, Hidetaka Gouzu, Shigeyuki Yokoyama, Shuji Ikeda, Hiroshi Sugiyama, and Masami Hagiya: State Transitions by Molecules, Preliminary Proceedings, Fourth International Meeting on DNA Based Computers, June 15 - June 19, 1998, University of Pennsylvania, pp.87-99. Also in BioSystems, Vol.52, No.1-3, 1999, pp.81-91.
  79. * Wei-Ngun Chin and Masami Hagiya: A Bounds Inference Method for Vector-Based Memoization, International Conference on Functional Programming '97, 1997, pp.176-187.

  80. * Yasuaki Takebe and Masami Hagiya: A User Interface for Controlling Term Rewriting Based on Computing-as-Editing Paradigm, User Interfaces for Theorem Provers UITP'97, INRIA Sophia-Antipolis, 1997, pp.93-100.

  81. Akira Suyama, Masanori Arita and Masami Hagiya: A Heuristic Approach for Hamiltonian Path Problem with Molecules, Genetic Programming 1997: Proceedings of the Second Annual Conference (John R. Koza, et al. eds.), Morgan Kaufmann, 1997, pp.457-462
  82. Masami Hagiya, Masanori Arita, Daisuke Kiga, Kensaku Sakamoto and Shigeyuki Yokoyama: Towards Parallel Evaluation and Learning of Boolean $\mu$-Formulas with Molecules, Preliminary Proceedings, 3rd DIMACS Workshop on DNA Based Computers, June 23 - June 25, 1997, University of Pennsylvania, pp.105-114. Also in DNA Based Computers III, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol.48, 1999, pp.57-72.
  83. Masanori Arita, Masami Hagiya and Akira Suyama: Joining and Rotating Data with Molecules, Proceedings of 1997 IEEE International Conference on Evolutionary Computation (ICEC'97), 1997, pp.243-248.
  84. * Masami Hagiya and Hiroshi Kakuno: Proving as Editing, User-Interfaces for Theorem Provers UITP'96, Department of Computer Science, University of York, 1996, pp.35-42.

  85. * Mituharu Yamamoto, Shin-ya Nishizaki, Masami Hagiya and Yozo Toda: Formalization of Planar Graphs, Higher-Order Logic Theorem Proving and Its Applications, Lecture Notes in Computer Science, Springer-Verlag, Vol.971, 1995, pp.369-384.

  86. * Masami Hagiya and Kouhei Iino: Binding Time Analysis for Data Type Specialization, Fuji International Workshop on Functional and Logic Programming, World Scientific, 1995, pp.254-269.

  87. Masami Hagiya and Tomoki Shiratori: Programming by Example in Computing-as-Editing Paradigm, Proceedings of the 11th International IEEE Symposium on Visual Languages, 1995, pp.275-283.

  88. Tomoaki Shimada, Masami Hagiya, Masanori Arita, Shin-ya Nishizaki and Chew Lim Tan: Knowledge-Based Simulation of Regulatory Action in Lambda Phage, First International IEEE Symposium on Intelligence in Neural and Biological Systems (INBS 95), 1995, pp.92-99. Also in International Journal of Artificial Intelligence Tools, Vol.4, No.4, December 1995, pp.511-524.
  89. Masanori Arita, Masami Hagiya and Tomoki Shiratori: GEISHA System: An Environment for Simulating Protein Interaction, Genome Informatics Workshop V, 1994, pp.80-89.
  90. * Wei-Ngan Chin and Masami Hagiya: Tupling and Lambda Abstraction yield Dynamic-Sized Tabulation, Acta Informatica, Vol.32, 1995, pp.93-115.

  91. Masami Hagiya and Yozo Toda: On Implicit Arguments, Logic, Language and Computation --- Festschrift in Honor of Satoru Takasu, Lecture Notes in Computer Science Vol.792, 1994, pp.10-30. The revised version is in TR-95-1 from Department Information Science, University of Tokyo.

  92. Akira Suyama, Masami Hagiya, Takashi Ito, Asao Fujiyama, Akira Ohyama, Toshihisa Takagi: ContigMaker: Software Tool for Contig Map Construction, Genome Informatics Workshop IV, 1993, pp.376-384.
  93. Masami Hagiya: A Deductive Method for Construction and Visualization of Contigs in the STS Strategy, Genome Informatics Workshop IV, 1993, pp.65-72.
  94. Masami Hagiya: A Typed lambda-Calculus for Priving-by-Example and Bottom-Up Generalization Procedure, Algorithmic Learning Theory (K. P. Jantke, S. Kobayashi, E. Tomita and T. Yokomori eds.), Lecture Notes in Artificial Intelligence, Vol.744, 1993, pp.73-86. Also in Theoretical Computer Science, Vol.137, 1995, pp.3-23.

  95. Masami Hagiya: An iterative and bottom-up procedure for proving-by-example, Machine Learning: ECML-93 (Pavel B. Brazdil ed.), Lecture Notes in Artificial Intelligence, Vol.667, 1993, pp.336-341.

  96. Masami Hagiya: A formal approach to visual proving based on logic programming, Proceedings of the 1992 IEEE Workshop on Visual Languages, Seattle, Washington, 1992, pp.234-236.

  97. Masami Hagiya: Higher-order unification as a theorem proving procedure, Eighth International Conference on Logic Programming, MIT Press, 1991, pp.270-284.

  98. S. Liu and M. Hagiya: Model inference of constrained recursive figures, Proceedings of the First International Workshop on Algorithmic Learning Theory, OHMSHA Ltd., 1990, pp.355-367.

  99. Masami Hagiya: Synthesis of rewrite programs by higher-order and semantic unification, Proceedings of the First International Workshop on Algorithmic Learning Theory, 1990, pp.396-410. Also in New Generation Computing, Vol.8, No.4, 1991, pp.403-420.

  100. Masami Hagiya: Programming by example and proving by example using higher-order unification, 10th Conference on Automated Deduction (M. E. Stickel ed.), Lecture Notes in Aritifical Intelligence, Vol.448, 1990, pp.588-602.

  101. M. Hagiya and K. Ohtani: Parallel object-oriented UIMS with macro and micro stubs, Proceedings of the Winter 1990 USENIX Conference, 1990, pp.259-273.

  102. M. Hagiya, T. Hattori, A. Morishima, R. Nakajima, N. Niide, R. Okazaki, T. Sakuragawa, T. Suzuki, H. Tsuiki and T. Yuasa: Overview of GMW+Wnn system, Advances in Software Science and Technology, Vol.1, 1989, pp.133-156.

  103. Masami Hagiya: Meta-circular interpreter for a strongly typed language, Journal of Symbolic Computation, Vol.8, No.12, 1989, pp.651-680. This is the main Ph.D work.

  104. Masami Hagiya: Generalization by parametrization in higher order type theory, Theoretical Computer Science, Vol.63, 1989, pp.113-139.

  105. M. Hagiya, T. Hattori, A. Morishima, R. Nakajima, N. Niide, R. Okazaki, T. Sakuragawa, T. Suzuki, H. Tsuiki and T. Yuasa: Overview of GMW+Wnn system, Proceedings of 2nd IEEE International Conference on Computer Workstations, 1988, pp.170-177.

  106. Masami Hagiya and Takafumi Sakurai: Foundation of logic programming based on inductive definition, New Generation Computing, Vol.2, 1984, pp.59-77.

  107. Masami Hagiya: A proof description language and its reduction system, Publications of the Research Institute for Mathematical Sciences, Kyoto University, Vol.19, No.1, 1983, pp.237-261. This is the M.Sc. work.

  108. Masahiko Sato and Masami Hagiya: Hyperlisp, Algorithmic Languages (J.W. de Bakker and J.C. van Vliet eds.), North-Holland, 1981, pp.251-269.

Invited Papers

  1. * S. Murata, A. Konagaya, S. Kobayashi, H. Saito, and M. Hagiya: Molecular Robotics: A New Paradigm for Artifacts, New Generation Computing, Vol.31, 2013, pp.27-45.
  2. Kazufumi Mizunuma and Masami Hagiya: Hybrid Method for Simulating Small-Number Molecular Systems, Algorithmic Bioprocesses (A. Condon, D. Harel, J. N. Kok, A. Salomaa, E. Winfree, Eds.), Natural Computing Series, Springer, 2009, pp.607-622.
  3. Masami Hagiya, Satsuki Yaegashi, and Keiichiro Takahashi: Computing with Hairpins and Secondary Structures of DNA, Nanotechnology: Science and Computation (Junghuei Chen, Natasha Jonoska, Grzegorz Rozenberg, Eds.) Natural Computing Series, Springer, 2005, pp.293-308.
  4. * Masami Hagiya, Koichi Takahashi, Mitsuharu Yamamoto and Takahiro Sato: Analysis of Synchronous and Asynchronous Cellular Automata using Abstraction by Temporal Logic, FLOPS2004: The Seventh Functional and Logic Programming Symposium, Lecture Notes in Computer Science, Vol.2998, 2004, pp.7-21.

  5. J. A. Rose, M. Takano, M. Hagiya and A. Suyama: A DNA Computing-based Genetic Program for in vitro Protein Evolution via Constrained Pseudomodule Shuffling, Journal of Genetic Programming and Evolvable Machines, Vol.4, 2003, pp.139-152.
  6. * Masami Hagiya: Towards Molecular Programming - a Personal Report on DNA8 and Molecular Computing, Modelling in Molecular Biology (G. Ciobanu, G. Rozenberg, Eds.), Natural Computing Series, Springer, 2004, pp.125-140.
  7. J. A. Rose, R. J. Deaton, M. Hagiya, and A. Suyama: A DNA-based in vitro Genetic Program, Journal of Biological Physics, Vol.28, 2002, pp.493-498.
  8. Masami Hagiya, John A. Rose, Ken Komiya, and Kensaku Sakamoto: Complexity analysis of the SAT engine: DNA algorithms as probabilistic algorithms, Theoretical Computer Science, Vol.287, 2002, pp.59-71.
  9. * Masami Hagiya: From Molecular Computing to Molecular Programming, DNA Computing, 6th International Workshop on DNA-Based Computers, DNA 2000, (Anne Condon and Grzegorz Rozenberg Eds.), Lecture Notes in Computer Science, Vol.2054, 2001, pp.89-102.
  10. * Masami Hagiya and Koichi Takahashi: Discovery and Deduction, Discovery Science, Third International Conference, DS 2000, (Setsuo Arikawa and Shinichi Morishita Eds.), Lecture Notes in Artificial Intelligence, Vol.1967, 2000, pp.17-37.

  11. Masami Hagiya: Perspectives on Molecular Computing, New Generation Computing, Vol.17, No.2, 1999, pp.131-140.
  12. * Masami Hagiya: Towards Autonomous Molecular Computers, Genetic Programming 1998: Proceedings of the Third Annual Conference (John R. Koza, et al. eds.), Morgan Kaufmann, 1998, pp.691-699.
  13. Masami Hagiya: From programming-by-example to proving-by-example, Theoretical Aspects of Computer Software (T. Ito and A. R. Meyer eds.), Lecture Notes in Computer Science, Vol.526, 1991, pp.387-419.

Unrefereed Papers (including Unpublished Papers)

  1. Cyrille Artho, Watcharin Leungwattanakit, Masami Hagiya, Yoshinori Tanabe, Eric Platon, Mitsuharu Yamamoto: Cache-based Model Checking of Networked Software, DNSA 2010 - The Workshop on Dependability of Network Software Applications, 2010.

  2. Vinh Cuong Tran, Yoshinori Tanabe and Masami Hagiya: Abstract Model Checking of Web Applications Using Java PathFinder, JSSST 2009, Japan Society for Software Science and Technology, 2009.

  3. Yoshinori Tanabe and Masami Hagiya: Games and Natural Number-valued Semantics of the Modal $\mu$-calculus, JSSST 2009, Japan Society for Software Science and Technology, 2009.

  4. Yusuke Kawamoto, Hideki Sakurada and Masami Hagiya: Generic Result for Mapping Soundness of Symbolic Signature Primitives, JSSST 2008, Japan Society for Software Science and Technology, 2008.

  5. Vinh Cuong Tran, Hideki Hashimoto, Tanabe Yoshinori and Masami Hagiya: Verification of Java programs under fairness assumption, JSSST 2008, Japan Society for Software Science and Technology, 2008.

  6. Mitsuharu Yamamoto, Yoshinori Tanabe, Koichi Takahashi, and Masami Hagiya: Abstraction of Graph Transformation Systems by Temporal Logic and Its Verification, IFIP TC2, Verified Software: Theories, Tools, Experiments, 2005.

  7. * Seika Abe, Masami Hagiya and Takao Nakajima: Code Generation for a DNA Computer by Integer Linear Programming, Proceedings of the 2004 IEEE Conference on Cybernetics and Intelligent Systems, Singapore, 1-3 December, 2004, pp.268-273.
  8. Keiichiro Takahashi and Masami Hagiya: Preliminary Experiments on Hairpin Structure Dissociation for Constructing Robust DNA Machines, Proceedings of the 2004 IEEE Conference on Cybernetics and Intelligent Systems, Singapore, 1-3 December, 2004, pp.285-290.
  9. Masami Hagiya: DNA Nanorobotics and Sequence Design, Proc. SICE Annual Conference, Sapporo, 2004, pp.2774-2778.
  10. Keiichiro Takahashi and Masami Hagiya: On Computation of Minimum Free Energy and Partition Function of Multiple Nucleic Acid Sequences, FIT2004, Forum on Information Science and Technology, 2004, Vol.1, pp.91-92.
  11. Hiroki Uejima and Masami Hagiya: Analyzing Secondary Structure Transition Paths of DNA/RNA Molecules, DNA9, Ninth International Meeting on DNA Based Computers, Preliminary Proceedings, 2003, pp.92-96. Also in DNA Computing, 9th International Workshop on DNA-Based Computers, DNA9, Madison, WI, USA, June 2003, Revised Papers, Lecture Notes in Computer Science, Springer, Vol.2943, 2004, pp.86-90.
  12. Atsushi Kameda, Masahito Yamamoto, Hiroki Uejima, Masami Hagiya, Kensaku Sakamoto and Azuma Ohuchi, Conformational Addressing using the hairpin structure of single-strand DNA, DNA9, Ninth International Meeting on DNA Based Computers, Preliminary Proceedings, 2003, pp.197-201. Also in DNA Computing, 9th International Workshop on DNA-Based Computers, DNA9, Madison, WI, USA, June 2003, Revised Papers, Lecture Notes in Computer Science, Springer, Vol.2943, 2004, pp.219-224.
  13. Mitsuharu Yamamoto and Masami Hagiya: Abstract A* Algorithm and Its Application to Linearly Priced Timed Automata, Proceedings of The Second Asian Workshop on Programming Languages and Systems (APLAS 2001), ROPAS Technical Memorandum 2001-16, KAIST (Korea Advanced Institute of Science and Technology), December 17-18, 2001, pp.193-205.

  14. Masami Hagiya, Mitsuharu Yamamoto and Jean-Marie Cottin: Symbolic Analysis of Timed Multiset Rewriting and Its Application to Protocol Analysis (Extended Abstract), Rewriting in Proof and Computation, International Workshop, RPC'01, The Research Institute of Electrical Communication (RIEC), Tohoku University, October 25-27, 2001, pp.34-41.

  15. * Masami Hagiya and Koichi Takahashi: Searching for Synchronization Algorithms using BDDs, IPSJ PRO, Information Processing Society of Japan, January 2001.

  16. John A. Rose, Akira Suyama, Masami Hagiya and Russel J. Deaton: An Antisense Antidote for Whiplash PCR, IPSJ Symposium Series, Vol.2000, No.16, Information Processing Society of Japan, 2000, pp.101-108.
  17. * Koichi Takahashi and Masami Hagiya: Abstraction of Link Structures by Regular Expressions and Abstract Model Checking of Concurrent Garbage Collection, First Asian Workshop on Programming Languages and Systems, National University of Singapore, 2000, pp.1-8.

  18. * Koichi Takahashi, Yozo Toda and Masami Hagiya: Nonce Analysis and Strand Space Model, JSSST 2000, Japan Society for Software Science and Technology, 2000.

  19. Akihiko Tozawa and Masami Hagiya: New Formalization of the JVM, 2000.

  20. * Masami Hagiya, Yozo Toda and Yoshiki Fukuba: Implementation and Verification of Authentication Protocols, Using Proof Procedures in HOL, Workshop on Enterprise Security (SSR99), Science University of Tokyo, November 11, 1999.

  21. Koichi Takahashi and Masami Hagiya: Verification of Parallel Garbage Collection by Abstract Model Checking, 1999.

  22. * Masami Hagiya: On a New Method for Dataflow Analysis of Java Virtual Machine Subroutines, IPSJ PRO, Information Processing Society of Japan, PRO-17-3, 1998, pp.13-18. The longer and newer version is here.

  23. Masami Hagiya: Unification and Inductive Theorem Proving by Transformation of Equations with Recursors, JSSST'96, Japan Society for Software Science and Technology, 1996, pp.97-100.

  24. Masami Hagiya, Hiroshi Watanabe and Toshiko Kitamura: On Merging Resolution and Induction, IPSJ PRO, Information Processing Society of Japan, PRO-6-12, 1996, pp.67-72.

  25. Masanori Arita, Masami Hagiya and Tomoki Shiratori: SIMFLY: The Simulation of a Fly Embryo, Genome Informatics Workshop V, 1994, pp.230-231.

  26. Akira Suyama, Akira Ohyama, Masami Hagiya, Yoshiaki Furuhata, Takashi Ito, Asao Fujiyama, Masahira Hattori, Yoshiyuki Sakaki, Toshihisa Takagi: ContigMaker and SAND: Software Tools for Genome Mapping and Sequencing, Genome Informatics Workshop V, 1994, pp.198-199.

  27. Masami Hagiya: On Reduction and Projection in Type Theory with Inductive Definitions, 12th International Conference on Automated Deduction, Workshop 1B: Proof Search in Type-Theoretic Languages, 1994, pp.31-38.

  28. Masami Hagiya: Running Higher-Order Unification in PaiLisp, Parallel Symbolic Computing: Languages, Systems, and Applications (Robert H. Halstead, Jr., Takayasu Ito, eds.), Lecture Notes in Computer Science, Vol.748, 1993, pp.155-160.

  29. Masami Hagiya: Boomborg-PC: A Proof-Checker of Calculus of Constructions Running on a Buffer of GNU Emacs, Department of Information Science, University of Tokyo, 1992, 1995.

  30. Masami Hagiya: An Operational Approach to Type Safety, 1992.

  31. Masami Hagiya: Explanation-based Generalization in Logical Framework, 1989.

  32. Masami Hagiya: Theory of Modal Logic Programming, 1985.

Tutorials

  1. Masami Hagiya: Implementations of computational state transitions with biomolecules, Scholarpedia, 6(4):9917, 2011.
  2. * Masami Hagiya: Information Technology for Synthetic Biology, The 20th International Conference on Genome Informatics (GIW 2009), 2009.
  3. Masami Hagiya: Molecular Computation Using Hairpins and Secondary Structures of DNA, Handbook of Theoretical and Computational Nanotechnology, Vol.6, Chapter 18, American Scientific Publishers, 2007, pp.817-840
  4. Masami Hagiya: Program Synthesis --- Past, Present and Future, InfoJapan 90, Information Processing Society of Japan, 1990.

Books (including Books Edited)

  1. Christian S. Calude, Masami Hagiya, Kenichi Morita, Grzegorz Rozenberg and Jon Timmis: Unconventional Computation, 9th International Conference, UC2010, Tokyo, Japan, June 2010, Proceedings, Lecture Notes in Computer Science, Vol.6079, Springer, 2010.

  2. Y. Suzuki, M. Hagiya, H. Umeo and A. Adamatzky: Natural Computing, 2nd International Workshop on Natural Computing, Nagoya, Japan, December 2007, Proceedings, Proceedings in Information and Communication Technology, PICT1, Springer, 2008.

  3. Masami Hagiya and Philip Wadler: Functional and Logic Programming, 8th International Symposium, FLOPS 2006, Fuji-Susono, Japan, April 2006, Proceedings, Lecture Notes in Computer Science, Vol.3945, Springer, 2006.

  4. Masami Hagiya and Azuma Ohuchi: DNA Computing, 8th International Workshop on DNA-Based Computers, DNA8, Sapporo, Japan, June 2002, Revised Papers, Lecture Notes in Computer Science, Vol.2568, Springer, 2003.
  5. J. van Leeuwen, O. Watanabe, M. Hagiya, P.D. Mosses, and T. Ito: Theoretical Computer Science, Exploring New Frontiers of Theoretical Informatics, Lecture Notes in Computer Science, Vol.1872, Springer-Verlag, 2000.

  6. Neil D. Jones, Masami Hagiya and Masahiko Sato: Logic, Language and Computation --- Festschrift in Honor of Satoru Takasu, Lecture Notes in Computer Science, Vol.792, Springer-Verlag, 1994.

  7. Masami Hagiya and John C. Mitchell: Theoretical Aspects of Computer Software --- International Symposium TACS'94, Sendai, Japan, April 1994, Proceedings, Lecture Notes in Computer Science, Vol.789, Springer-Verlag, 1994.

  8. Ikuo Nakata and Masami Hagiya: Software Science and Engineering --- Selected Papers from the Kyoto Symposia, World Scientific, 1991.

  9. Taiichi Yuasa and Masami Hagiya: Introduction to Common Lisp, Academic Press, Inc., 1987.

Lecture Notes

  1. Verification of Computing Systems


Software

Hack and perish!

Original Software

  1. MediaWiki for Molecular Robotics and Synthetic Biology with Ibuki Kawamata and Satoshi Egi.
  2. net-iocache with Watcharin Leungwattanakit, Cyrille Artho, et al.
  3. Supporting SBUML by Richard Potter.
  4. VNA: Simulator for Virtual DNA Experiments with Akio Nishikawa.
  5. Boomborg-HOL with Koichi Takahashi.
  6. Boomborg-KEISAN with Tomoki Shiratori.
  7. SIMFLY with Masanori Arita and Tomoki Shiratori.
  8. ContigMaker with Akira Suyama et al.
  9. Boomborg-PC helped by Yozo Toda and Mitsuharu Yamamoto.
  10. G Strikes Back with Koji Otani and many people.
  11. Gimme More Windows with Koji Otani and many people.
  12. Kyoto Common Lisp with Taiichi Yuasa.
  13. Prolog11P.
  14. Hyperlisp with Masahiko Sato.


International Activities

Program Committee (not exhaustive)

Editorial Board


Short Personal History



Publications in Japanese

Papers (Refereed)

  1. 今井健男, 酒井政裕, 萩谷昌己: Minimal Unsatisfiable Core列挙によるプログラムの準最弱な事前条件推定, ソフトウェア工学の基礎XVIII, レクチャーノート/ソフトウェア学, 近代科学社, Vol.37, 2011, pp.187-196. Also in コンピュータソフトウェア, Vol.30, No.2, 2013, pp. 207-226.

  2. 川本裕輔, 真野健, 櫻田英樹, 萩谷昌己: 関数部分知識と匿名性検証, 日本応用数理学会論文誌, Vol.17, No.4, 2007, pp.559-576. (日本応用数理学会論文賞(理論部門)受賞)

  3. 萩谷昌己: 数理的技法による情報セキュリティの検証, 応用数理, Vol.17, No.4, 2007, pp.8-15.

  4. 齋藤孝道, 鬼頭利之, 萩谷昌己, 溝口文雄: SSHパスワードユーザ認証の脆弱性とその考察, 情報処理学会論文誌, Vol.47, No.4, 2006, pp.1118-1126.

  5. 田辺良則, 高橋孝一, 山本光晴, 佐藤貴洋, 萩谷昌己: BDDを用いた2方向CTL論理式充足可能性決定手続きの実装, コンピュータソフトウェア, Vol.22, No.3, 2005, pp.154-166.

  6. 阿部正佳, 萩谷昌己: 整数線形計画法を用いたDNAコンピュータ制御コードの生成, 情報処理学会論文誌プログラミング, Vol.45, No.SIG9(PRO22), 2004, pp.1-13.

  7. 萩谷昌己, 竹村亮, 高橋孝一, 齋藤孝道: 束縛関係に基づく認証プロトコルの検証, コンピュータソフトウェア, Vol.20, No.3, 2003, pp.17-29.

  8. 戸沢晶彦, 萩谷昌己: JAVA2のPermission機構のモデル化と実験, コンピュータソフトウェア, Vol.18, No.6, 2001, pp.43-53.

  9. 萩谷昌己, 高橋孝一: モデル検査系を用いたプログラム発見, 人工知能学会誌, Vol.16, No.5, 2001, pp.648-654.

  10. 齋藤孝道, 萩谷昌己, 溝口文雄: 公開鍵を用いた認証プロトコルについて, 情報処理学会論文誌, Vol.42, No.8, 2001, pp.2040-2048.

  11. 高橋孝一, 萩谷昌己: 正則表現を用いた並列ごみ集めの抽象モデル検査, 情報処理学会論文誌プログラミング, Vol.42, No.SIG2(PRO9), 2001, pp.61-70.

  12. 山本光晴, 高橋孝一, 萩谷昌己, 西崎真也, 玉井哲雄: グラフ探索アルゴリズムの発展とその応用, コンピュータソフトウェア別冊, ソフトウェア発展, Vol.19, No.0, 2001, pp.92-108.

  13. 萩谷昌己, 戸沢晶彦, 高橋孝一, 西崎真也: Javaのクラスローダ制約の定式化, 情報処理学会論文誌プログラミング, Vol.41, No.SIG4(PRO7), 2000, pp.79-87.

  14. 山下大輔,高木啓伸,萩谷昌己: 「賢い紙」・紙に埋め込まれたプログラムによる紙インタフェースの提案, インタラクティブシステムとソフトウェアVII, レクチャーノート/ソフトウェア学, 近代科学社, Vol.23, 1999, pp.17-22.

  15. 戸田洋三, 萩谷昌己: タクティクからのプログラム抽出とその応用, 情報処理学会論文誌プログラミング, Vol.40, SIG4(PRO3), 1999, pp.21-32.

  16. 萩谷昌己, 高橋孝一: 「計算=編集」パラダイムに従うHOLタクティクのためのEmacsインタフェース, インタラクティブシステムとソフトウェアV, レクチャーノート/ソフトウェア学, 近代科学社, Vol.18, 1997, pp.123-128.

  17. 竹辺靖昭, 萩谷昌己: CAEPに基づいた項書き換え制御のユーザインタフェース, インタラクティブシステムとソフトウェアIV, レクチャーノート/ソフトウェア学, 近代科学社, Vol.16, 1996, pp.31-40.

  18. 萩谷昌己, 白取知樹: 「計算=編集」パラダイムに基づく例によるプログラミング, コンピュータソフトウェア, Vol.13, No.3, 1996, pp.64-78. (日本ソフトウェア科学会論文賞受賞)

  19. 山本光晴, 萩谷昌己, 白取知樹, 西崎真也: 図的対象を扱う証明チェッカのための視覚化ツール インタラクティブシステムとソフトウェアIII, レクチャーノート/ソフトウェア学, 近代科学社, Vol.12, 1995, pp.85-92.

  20. 角野宏司, 有田正規, 萩谷昌己, 白取知樹: Computing-as-Editing(CAEP)に基づいた 数式処理システムのユーザ・インタフェース, インタラクティブシステムとソフトウェアIII, レクチャーノート/ソフトウェア学, 近代科学社, Vol.12, 1995, pp.161-170.

  21. 加藤和彦, 萩谷昌己, 千葉滋, 綾塚裕二, 益田隆司: オブジェクト指向データベースを用いた グラフィカルユーザインターフェースシステムについて, アドバンスト・データベースシステム・シンポジウム, 情報処理学会, 1992.

  22. 萩谷昌己: 高階単一化と証明の一般化, 人工知能学会誌, Vol.6, No.3, 1991, pp.388-396.

  23. 大谷浩司, 角野宏司, 児島彰, 萩谷昌己, 服部隆志, 劉樹苓: GMWウィンドウ・システム上のアプリケーション構築について, コンピュータソフトウェア, Vol.7, No.1, 1990, pp.45-60.

Papers (Invited)

  1. 萩谷昌己: DNAロボットの自動設計に向かって ― DNAナノテクノロジーと合成生物学と情報科学 ―, 計測自動制御学会, システム情報部門講演会 (SSI09), 2009.
  2. 萩谷昌己, 山村雅幸: 分子プログラミング, ソフトウェア工学の基礎XIV, レクチャーノート/ソフトウェア学, 近代科学社, Vol.33, 2007, pp.1-4.
  3. 萩谷 昌己: 大容量DNAメモリとランダム性の活用, 数理モデル化と問題解決シンポジウム, ISSN 1344-0640, 情報処理学会シンポジウムシリーズ, Vol.2006, Nol.10, 2006 pp.9-16.
  4. 萩谷 昌己: 分子コンピュータの理論と構築, 人工知能学会全国大会(第11回)論文集, 1997, pp.9-17.

Papers (Unrefereed)

  1. 田辺良則, Cyrille Artho, Watcharin Leungwattanakit, 山本光晴, 萩谷昌己: ネットワークアプリケーションの マスター・スレーブ方式モデル検査アルゴリズムについて, 日本ソフトウェア科学会第28回大会, 2011.

  2. 櫻田英樹, 川本裕輔, 萩谷昌己: 能動的攻撃者の下でのXORの記号モデルとその計算論的健全性, 日本応用数理学会2009年度年会講演予稿集, 2010.

  3. 田辺良則, Cyrille Artho, 萩谷昌己, Watcharin Leungwattanakit, 山本光晴: ネットワークアプリケーションのマスタースレーブ方式によるソフトウェアモデル検査, 第8回ディペンダブルシステムワークショップ, 日本ソフトウェア科学会ディペンダブルシステム研究会, 2010.

  4. ウベール・コモン-ルンド, 萩谷昌己, 川本裕輔, 櫻田英樹: 計算論的に健全な記号的匿名性, 日本応用数理学会2009年度年会講演予稿集, 2009.

  5. 川本裕輔, 櫻田英樹, 萩谷昌己: リング署名の計算論的に健全な形式化, 日本応用数理学会2008年度年会講演予稿集, 2008, pp.179-180.

  6. 萩谷昌己: Excelでプログラムを書く, 夏のプログラミング・シンポジウム, 「First Programming Languages プログラミング言語の実力と美学」報告集, 情報処理学会, 2008, pp.5-11.

  7. 櫻田英樹, 萩谷昌己: ブラインド署名を扱うことが可能な計算論的に健全なプロトコル検証法, 日本応用数理学会2007年度年会講演予稿集, 2007, pp.42-43.

  8. 五十嵐大, 田辺良則, 西澤弘毅, 萩谷昌己: min-plus代数N上の様相μ計算とその応用, 日本ソフトウェア科学会第24回大会, 2007.

  9. 田辺良則, 萩谷昌己: 階層的グラフ構造の記述と検証のための様相論理, 日本ソフトウェア科学会第23回大会, 2006.

  10. 川本裕輔, 真野健, 櫻田英樹, 萩谷昌己: 電子投票プロトコルの匿名性検証のための関数部分知識モデル, 日本ソフトウェア科学会第23回大会, 2006.

  11. 櫻田英樹, 萩谷昌己: 遷移関係の詳細化による正則モデル検査の再構成と拡張, 日本ソフトウェア科学会第23回大会, 2006.

  12. 阿部正佳, 萩谷昌己, 瀬川修: DNA コンピュータ制御コードの最適化, 日本ソフトウェア科学会第22回大会, 2005.

  13. 山本光晴, 萩谷昌己: 時相論理による抽象化を用いた検証とその応用, 日本ソフトウェア科学会第22回大会, 2005.

  14. 田辺良則, 高橋孝一, 山本光晴, 佐藤貴洋, 戸沢晶彦, 萩谷昌己: BDDによる実装が可能な様相論理の充足可能性判定手続き, 日本ソフトウェア科学会, PPL2005, 2005.

  15. 中川孔人, ポッター リチャード, 山本光晴, 萩谷昌己, 加藤和彦: SBUMLとGDBの連携によるマルチプロセスアプリケーションのモデル検査, 第2回ディペンダブルソフトウェアワークショップDSW2005論文集, 日本ソフトウェア科学会研究会資料シリーズ, No.35, 2005, pp.13-21.

  16. 山本光晴, 萩谷昌己: 格子状の様相を持つ時相論理による抽象化のための充足可能性判定, 日本ソフトウェア科学会第21回大会, 2004.

  17. 佐藤貴洋, 田辺良則, 萩谷昌己: BDDを用いたガード付きフラグメントの充足可能性判定, 日本ソフトウェア科学会第21回大会, 2004.

  18. 中川孔人, 萩谷昌己, ポッターリチャード: SBUMLを用いたOSレベルでのUndoの実現とその応用, 日本ソフトウェア科学会第21回大会, 2004.

  19. 萩谷昌己, 高橋孝一, 山本光晴, 佐藤貴洋: 時相論理による抽象化を用いたセル・オートマトンの解析, 日本ソフトウェア科学会第20回大会, 2003.

  20. 松下耕三, 萩谷昌己: 携帯電話上における証明付き認証, 日本ソフトウェア科学会第20回大会, 2003.

  21. 萩谷昌己: グラフ書き換えと時空間様相論理, 情報処理学会, プログラミング研究会, 2003.

  22. 西澤 弘毅, 萩谷 昌己: Linear Logical Framework の拡張による Local Model Checking の形式的検証, 日本ソフトウェア科学会第19回大会, 2002.

  23. * 萩谷昌己, 山本光晴, ジャン-マリ コタン: 時間付き多重集合書き換えに対する記号的解析とそのプロトコル解析への応用, 日本ソフトウェア科学会第18回大会, 2001.

  24. * 山本光晴, 萩谷昌己: 抽象到達可能性検査のPriced Timed Automatonへの応用, 日本ソフトウェア科学会第18回大会, 2001.

  25. 萩谷昌己, 高橋孝一: 証明の表現, 夏のプログラミングシンポジウム「計算機と表現」報告集, 2000年8月30日〜9月1日, 情報処理学会, 2001, pp.89-92.

  26. 萩谷昌己, 小宮健, 坂本健作: SAT Engineの計算量 --- 確率アルゴリズムとしてのDNAアルゴリズム ---, 新しい計算パラダイムシンポジウム2000 論文集, 情報処理学会シンポジウムシリーズ, Vol.2000, No.16, 2000, pp.109-114.
  27. 坂本健作, 小宮健, 横山茂之, 萩谷昌己: DNA分子の自己会合反応の解析, 新しい計算パラダイムシンポジウム2000 論文集, 情報処理学会シンポジウムシリーズ, Vol.2000, No.16, 2000, pp.115-121.
  28. 萩谷昌己: 格子モデルによるヘアピン形成のシミュレーション, 新しい計算パラダイムシンポジウム2000 論文集, 情報処理学会シンポジウムシリーズ, Vol.2000, No.16, 2000, p.85.
  29. 山下大輔,高木啓伸,萩谷昌己: オフライン紙ユーザインタフェースのための例による図形認識プログラミング, インタラクティブシステムとソフトウェアVIII, レクチャーノート/ソフトウェア学, 近代科学社, Vol.24, 2000, pp.253-254.

  30. 高橋孝一, 戸田洋三, 萩谷昌己: ノンス解析とストランド空間モデル, 日本ソフトウェア科学会第17回大会論文集, 2000. English version is here.

  31. 戸沢晶彦, 萩谷昌己: Java2のPermission機構のモデル化と実験, 第2回プログラミングおよびプログラミング言語ワークショップ, 日本ソフトウェア科学会, 2000.

  32. 萩谷昌己: 検証系を用いたアルゴリズムの発見, 第41回プログラミング・シンポジウム報告集, 情報処理学会, 2000, pp.9-19.

  33. 山本光晴, 高橋孝一, 萩谷昌己: モデル検査アルゴリズムの検証について, 日本ソフトウェア科学会第16回大会論文集, 1999, pp.337-344.

  34. 高橋孝一, 萩谷昌己: 定理証明における図的推論の健全な実装法, 日本ソフトウェア科学会第16回大会論文集, 1999, pp.81-84.

  35. 高橋孝一, 萩谷昌己: 抽象モデル検査による並列ごみ集めの検証, 第2回プログラミングおよび応用のシステムに関するワークショップ, SPA'99, 日本ソフトウェア科学会, 1999.

  36. 山本光晴, 萩谷昌己: 帰納的定義の発展, 日本ソフトウェア科学会第15回大会論文集, 1998, pp.405-408.

  37. 萩谷昌己, 高橋孝一, 西崎真也: Javaクラスローダの定式化とバイナリ互換性, 日本ソフトウェア科学会第15回大会論文集, 1998, pp.89-92.

  38. * 萩谷昌己: Java仮想機械手続きのための新しいデータフロー解析について, 第1回プログラミングおよび応用のシステムに関するワークショップ論文集, 日本ソフトウェア科学会, 1998. Also in 情報処理学会, プログラミング研究会, PRO-17-3, 1997.

  39. * 萩谷昌己, 山本光晴, 高橋孝一, 西崎真也, 玉井哲雄: グラフ探索アルゴリズムの形式化とその応用, 日本ソフトウェア科学会第14回大会論文集, 1997, pp.593-596.

  40. * 戸田洋三, 萩谷昌己: タクティクの一般化によるプログラム抽出, 日本ソフトウェア科学会第14回大会論文集, 1997, pp.561-564.

  41. 戸田洋三, 萩谷昌己: tacticからのプログラム抽出, 情報処理学会, プログラミング研究会, PRO-12-2, 1997, pp.9-14.

  42. 白取知樹, 萩谷昌己: 編集=計算パラダイムと例によるプログラミング, 情報処理学会, プログラミング研究会, PRO-3-1, 1995, pp.1-2.

  43. 萩谷昌己: 制約付き型理論の実現, 関数プログラミングII, JSSST'94, レクチャーノート/ソフトウェア学, 近代科学社, 1994, pp.63-77.

  44. 浅井弘子, 西崎真也, 萩谷昌己: 自然言語インターフェースを用いた検索結果の視覚化, 1993年度人工知能学会全国大会, 1993, pp.589-592.

  45. 萩谷昌己: テキスト・エディタ上の証明チェッカ, 情報処理学会, プログラミング-言語・基礎・実践-研究会, PRG-7-9, 1992.

  46. 萩谷昌己: 帰納的定義付き型理論における簡約と射影について, 情報処理学会, ソフトウェア基礎論研究会, SF-38-7, 1990.

  47. 萩谷昌己: 定理証明手続きとしての高階単一化, 情報処理学会, ソフトウェア基礎論研究会, SF-36-3, 1990.

  48. 萩谷昌己: オブジェクト指向言語における型の拡張性について, 日本ソフトウェア科学会第4回大会論文集, 1987, pp.151-154

  49. 萩谷昌己: GはGMWのG --- GMWウィンドウ・システムの拡張用言語Gについて, 情報処理学会, プログラミング言語研究会, PL-13-1, 1987.

  50. 萩谷昌己: 型のある言語におけるmeta-circularなインタープリタについて, 日本ソフトウェア科学会第3回大会論文集, 1986, pp.9-15.

  51. 萩谷昌己: 構成的型理論における一般化について, 日本ソフトウェア科学会第2回大会論文集, 1985, pp.189-192. (日本ソフトウェア科学会高橋奨励賞受賞)

  52. 湯浅太一, 萩谷昌己: Kyoto Common Lispの実現, 情報処理学会, 記号処理研究会, SYM-34-1, 1985.

  53. 湯淺太一, 萩谷昌己: Common Lispシステム実現上の問題点, 情報処理学会, 記号処理研究会, SYM-32-9, 1985.

  54. 萩谷昌己: Theory of Modal Logic Programming, 情報処理学会, ソフトウェア基礎論研究会, SF-9-4, 1984.

  55. 萩谷昌己: Prolog Shell ----Prolog with Modality, 情報処理学会, 記号処理研究会, SYM-28-2, 1983.

  56. 萩谷昌己: Lazy ReductionによるHAのNormalization, 情報処理学会第23回(昭和56年後期)全国大会, 1981, pp.31-32.

  57. 萩谷昌己, 佐藤雅彦: Hyperlispとそのimplementation, 情報処理学会, 記号処理研究会, SYM-14-3, 1980.

Tutorials

  1. 萩谷昌己: RubyのJIS規格化・ISO規格化を祝って, 情報処理, Vol.53, 2012, pp.838-841.

  2. 萩谷昌己: "情報"と"生命"が創発しあう時代 --- 合成生物学の背景にある知の力学, 科学, Vol.80, No.7, 岩波書店, 2010, pp.743-746.
  3. 萩谷昌己: 生命の「しかけ」で作る分子機械, じっきょう, No.25, 実教出版, 2009, pp.3-6.
  4. 萩谷昌己: 安心・安全な社会のためのゲームの話, 理大 科学フォーラム, 東京理科大学 科学教養誌, No4, 2009, pp.28-32.

  5. 萩谷昌己: 情報科学と論理,数理科学, Vol.46, No.11, 2008, pp.43-48.

  6. 萩谷昌己: フォーマルメソッドによる暗号安全性, 情報処理, Vol.49, No.5, 2008, pp.537-543.

  7. 萩谷昌己: 生命的コンピューティング, 人工知能学会誌, Vol.23, No.3, 2008, pp.404-414.
  8. 萩谷昌己: DNA鎖に基づくナノシステム, 高分子, Vol.56, No.6, 2007, p.440.
  9. 萩谷昌己: 数理的技法によるセキュリティプロトコルの検証, 日本応用数理学会2006年度年会講演予稿集, 2006, pp.8-11.

  10. 萩谷昌己: 大学入試における「情報」科目の導入へ向けて, じっきょう, No.17, 実教出版, 2007, pp.1-6.

  11. 萩谷昌己: 分子コンピューティングの発展 --- 分子マシンから分子コミュニケーションへ ---, 電子情報通信学会誌, Vol.89, No.6, 2006, pp.500-505.
  12. 萩谷昌己: 二次構造の解離に基づく汎用分子システム, シミュレーション, Vol.24, No.4, 2005, pp.21-24.
  13. 萩谷昌己: 分子プログラミング, 応用物理, Vol.74, No.7, 2005, pp.930-934.
  14. 萩谷昌己: ソフトウェア・セキュリティにおける理論研究の役割, 科学, Vol.74, No.2, 岩波書店, 2004, pp.185-190.

  15. 萩谷昌己: サイエンスへの招待: 分子コンピューティングのこと, 東京大学広報誌「淡青」, Vol.6, February, 2002, p.24.
  16. 萩谷昌己: 最近の分子コンピューティング, Computer Today, No.109, 2002, pp.4-10.
  17. 萩谷昌己, 有田正規: 分子計算とその物理学的基礎, 日本物理学会誌, Vol.56, No.6, 2001, pp.403-410.
  18. 萩谷昌己: 特集 未来予想 --- 2050年あるものないもの, コンピュータサイエンス, bit, Vol.33, No.11, 2001, pp.18-21.
  19. 萩谷昌己: 分子計算から分子プログラミングへ, 計測と制御, Vol.40, No.1, 2001, pp.100-105.
  20. 萩谷昌己, 米崎直樹: ソフトウェア発展と検証技術の未来, bit, Vol.32, No.12, 2000, pp.3-8.

  21. 萩谷昌己, 西川明男: DNA計算, 遺伝的アルゴリズム4, 第1章, 産業図書, 2000, pp.3-48
  22. 萩谷昌己, 西川明男: DNA計算とは何か, 電子情報通信学会誌, Vol.83, No.10, 2000, pp.756-762.
  23. 西川明男, 萩谷昌己: DNA計算のためのシミュレーションの試み, 数理科学, No.445, 2000年7月号, pp.15-26.
  24. 萩谷昌己: DNA計算の新基軸, 人工知能学会誌, Vol.15, No.1, 2000, pp.43-50.
  25. 萩谷昌己・西川明男: 分子計算から見た並行計算 -- Making Chemical Abstract Machines More Chemical --, 日本ファジィ学会誌, Vol.11, No.1, 1999, pp.2-13.
  26. 萩谷昌己: 計算システムの検証と合成, 学術月報, Vol.51, No.10, 1998, pp.10-14.

  27. 萩谷昌己: 生物の系のモデル化とシミュレーション: その意義と研究方向, 特集:「ゲノム情報」,情報処理, Vol.37, No.10, October 1996, pp.941-945.
  28. 萩谷昌己: 形式的数学のための計算機環境, 日本数学会年会, 特別講演, 1996.

  29. 萩谷昌己: 証明チェッカとそのユーザ・インターフェース, 人工知能学会誌, Vol.10, No.1, January 1995, pp.52-60.

  30. 萩谷昌己, 劉樹苓: 図形を用いた推論の基礎づけ, 人工知能学会誌, Vol.9, No.2, March 1994, pp.190-195.

  31. 萩谷昌己: 視覚的プログラミングと自動プログラミング, コンピュータソフトウェア, Vol.8, No.2, 1991, pp.27-39.

  32. 萩谷昌己: グラフィカルなユーザ・インタフェースとその開発環境について, bit, Vol.21, No.5, 1989, pp.51-62.

  33. 萩谷昌己, 森島晃年: ワークステーション上のウィンドウ・システムについて, コンピュータソフトウェア, Vol.5, No.2, 1988, pp.2-24.

  34. 萩谷昌己: GMWウィンドウ・システムについて, bit, Vol.19, No.3, 1987, pp.4-19.

  35. 湯浅太一, 萩谷昌己: KCl(Kyoto Common Lisp), コンピュータソフトウェア, Vol.1, No.2, 1984, pp.69-72.

  36. 萩谷昌己: Prologの基礎, 情報処理, Vol.25, No.12, 1984, pp.1336-1344.

  37. 萩谷昌己: よい子のはいぱーりすぷ, bit, Vol.14, No.3, 1982, pp.28-37.

Books (including Books Edited)

  1. 萩谷昌己, 横森貴編: ナチュラルコンピューティング・シリーズ, 近代科学社, 2011-.

  2. 萩谷昌己, 塚田恭章編: 数理的技法による情報セキュリティ, シリーズ応用数理1, 共立出版, 2010.

  3. 増原英彦, 東京大学情報教育連絡会: 情報科学入門―Rubyを使って学ぶ, 東京大学出版会, 2010.

  4. 萩谷昌己, 山本光晴: 化学系と生物系の計算モデル, アルゴリズム・サイエンス シリーズO, 共立出版, 2009.

  5. 川合慧, 萩谷昌己: 基礎情報科学, 放送大学大学院文化科学研究科, 日本放送出版協会, 2009.

  6. 萩谷昌己, 西川明男: DNAロボット--生命のしかけで創る分子機械, 岩波科学ライブラリー153, 岩波書店, 2008.
    訂正: p.20の図10の螺旋構造において、3'と5'がすべて逆です。 申し訳ありません。m(_ _)m
  7. 萩谷昌己監修, 吉岡信和, 青木利晃, 田原康之著: SPINによる設計モデル検証, 近代科学社, 2008.

  8. 萩谷昌己, 西崎真也: 論理と計算のしくみ, 岩波書店, 2007. 訂正と補足 (2008年度大川出版賞受賞)

  9. 岩波書店編集部編: 情報科学への道、情報科学の行く道, ブックガイド 文庫で読む科学, 岩波科学ライブラリー132, 2007, pp.105-114.

  10. 萩谷昌己編著: 分子コンピュータの現状と展望 -- 分子プログラミングへの展開, 臨時別冊・数理科学, SGCライブラリ31, サイエンス社, 2004.
  11. 萩谷昌己, 横森貴(共編): DNAコンピュータ, 培風館, 2001.
  12. 萩谷昌己: 関数プログラミング, 日本評論社, 1998.

  13. 萩谷昌己: ソフトウェア科学のための論理学, 岩波講座「ソフトウェア科学」, 第11巻, 1994.

  14. 萩谷昌己: 論理と計算, 岩波講座「応用数学」, 基礎11, 1993.

  15. 湯浅太一, 萩谷昌己: Common Lisp入門, 岩波書店, 1986. 英語訳 --- Introduction to Common Lisp, Academic Press, Inc., 1987.

  16. 湯浅太一, 萩谷昌己: Kyoto Common Lisp Report, 帝国印刷, 1985.

  17. 萩谷昌己: ソフトウェア考現学, CQ出版, 1985.

Lecture Notes

  1. 計算モデル論 東京大学理学部情報科学科4年「計算モデル論」, 2014年夏学期. 2013年夏学期. 2012年夏学期. 2011年夏学期. 2010年夏学期.

  2. フォーマルメソッドによる暗号プロトコルの検証 東京大学理学部情報科学科4年「計算機言語論」, 2009年夏学期, 東京大学大学院情報理工学系研究科「計算システム検証論」, 2008年冬学期.

  3. 様相論理・時相論理・モデル検査・Java PathFinder 東京大学理学部情報科学科4年「計算機言語論」, 2010年夏学期, 2009年夏学期, 2008年夏学期, 2007年夏学期, 2003年夏学期, 2002年夏学期, 2001年夏学期, 2000年夏学期, 1999年夏学期. 東京大学大学院情報理工学系研究科「計算システム検証論」, 2007年冬学期. 第一回プログラミングおよびプログラミング言語サマースクール, 日本ソフトウェア科学会・プログラミング論研究会, 2003. 筑波大学第三学群情報学類「情報科学特別講義ID」集中講義, 1999年2月20日, 3月6日.

  4. 情報論理 東京大学理学部情報科学科3年「情報論理」, 2010年夏学期, 2009年夏学期, 2008年夏学期, 2007年夏学期. 2006年夏学期, 2005年夏学期, 2004年夏学期.

  5. 情報科学, 東京大学教養学部「情報科学」 2010年冬学期, 2009年冬学期, 2008年冬学期, 2007年冬学期, 2006年冬学期, 東京大学教養学部総合科目「計算機プログラミングI」, 2004年夏学期.

  6. 形式的検証技術: Logical Framework と Modal Logic, 第5回「代数学と計算」研究集会(AC2003), 東京都立大学, 2003.

  7. 生物情報科学 東京大学理学部生物情報科学学部教育特別プログラム「生物情報科学概論」, 2005年夏学期, 2004年夏学期, 2003年夏学期, 2002年夏学期.
  8. 分子コンピューティング 東京大学理学部情報科学科4年「計算モデル論」, 2005年夏学期, 2004年夏学期. 東京大学理学部情報科学科4年「情報科学特別講義I」, 2003年夏学期. 東京大学理学部情報科学科4年「生命情報論」, 2002年夏学期.
  9. 状態探索による検証およびハイブリッド・システム 東京大学大学院情報理工学系研究科「計算システム検証論」, 2002年冬学期, 2001年冬学期.

  10. Javaとサーチ 東京大学教養学部総合科目「計算と知能の科学」, 2000年夏学期, 1999年夏学期.

  11. 再帰的関数とリスト処理, 東京大学教養学部総合科目「計算と知能の科学」, 1997年夏学期, 1996年夏学期.

  12. 帰納的定義と数学的帰納法(新版), 東京大学理学部情報科学科4年「計算機言語論」, 1998年夏学期, 1997年夏学期, 1996年夏学期. 筑波大学第三学群情報学類「人工知能I」集中講義, 1995年11月. 慶応大学「計算機科学特論」, 1995年11月. 付録: 山本光晴氏によるHOLを用いた検証 その解説.

  13. コンパイラ 東京大学理学部情報科学科3年「言語処理系論」, 2003年夏学期, 2002年夏学期, 2001年夏学期, 2000年夏学期, 1999年夏学期, 1998年夏学期, 1997年夏学期, 1996年夏学期. 東京大学理学部情報科学科3年「コンパイラ構成論」, 1995年冬学期, 1994年冬学期.

  14. 情報処理, 東京大学教養学部理科1類1年「情報処理」, 1996年夏学期, 1995年夏学期, 1994年夏学期.

  15. 帰納的定義と数学的帰納法(旧版), 東京大学理学部情報科学科4年「計算機言語論」, 1995年夏学期.

  16. 「構成的プログラミングと型付きλ計算」入門, 東京大学理学部情報科学科4年「計算機言語論」, 1995年夏学期. 筑波大学第三学群情報学類「人工知能I」集中講義, 1994年11月. 東京大学理学部情報科学科4年「計算機言語論」, 1994年夏学期.

Essays


学会など

受賞など

学歴

職歴