Mitsuhiro Okada

Koji Mineshima, Mitsuhiro Okada, Ryo Takemura: A Diagrammatic Inference System with Euler Circles. Journal of Logic, Language and Information 21(3): 365-391 (2012)

Koji Mineshima, Mitsuhiro Okada, Ryo Takemura: A Generalized Syllogistic Inference System based on Inclusion and Exclusion Relations. Studia Logica 100(4): 753-785 (2012)

Koji Mineshima, Mitsuhiro Okada, Ryo Takemura: Two Types of Diagrammatic Inference Systems: Natural Deduction Style and Resolution Style. Diagrams 2010: 99-114

Gergei Bana, Koji Hasebe, Mitsuhiro Okada: Secrecy-Oriented First-Order Logical Analysis of Cryptographic Protocols. IACR Cryptology ePrint Archive 2010: 80 (2010)

Gergei Bana, Koji Hasebe, Mitsuhiro Okada: Computational Semantics for First-Order Logical Analysis of Cryptographic Protocols. Formal to Practical Security 2009: 33-56

Véronique Cortier, Claude Kirchner, Mitsuhiro Okada, Hideki Sakurada (Eds.): Formal to Practical Security - Papers Issued from the 2005-2008 French-Japanese Collaboration. Lecture Notes in Computer Science 5458, Springer 2009, isbn 978-3-642-02001-8

Koji Mineshima, Mitsuhiro Okada, Yuri Sato, Ryo Takemura: Diagrammatic Reasoning System with Euler Circles: Theory and Experiment Design. Diagrams 2008: 188-205

Gergei Bana, Koji Hasebe, Mitsuhiro Okada: Computational Semantics for Basic Protocol Logic - A Stochastic Approach. ASIAN 2007: 86-94

Mitsuhiro Okada, Ryo Takemura: Remarks on Semantic Completeness for Proof-Terms with Laird's Dual Affine/Intuitionistic lambda -Calculus. Rewriting, Computation and Proof 2007: 167-181

Gergei Bana, Koji Hasebe, Mitsuhiro Okada: Computational Semantics for Basic Protocol Logic - A Stochastic Approach. IACR Cryptology ePrint Archive 2007: 156 (2007)

Koji Hasebe, Mitsuhiro Okada: Completeness and Counter-Example Generations of a Basic Protocol Logic: (Extended Abstract). Electr. Notes Theor. Comput. Sci. 147(1): 73-92 (2006)

Max I. Kanovich, Mitsuhiro Okada, Kazushige Terui: Intuitionistic phase semantics is almost classical. Mathematical Structures in Computer Science 16(1): 67-86 (2006)

Mitsuhiro Okada, Yutaro Sugimoto, Sumi Yoshikawa, Akihiko Konagaya: Drug Interaction Ontology (DIO) and the Resource-Sensitive Logical Inferences. Essays Dedicated to Joseph A. Goguen 2006: 616-642

Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada: The Calculus of Algebraic Constructions. CoRR abs/cs/0610063 (2006)

Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada: Inductive-data-type Systems. CoRR abs/cs/0610066 (2006)

Jean-Yves Girard, Mitsuhiro Okada, Andre Scedrov: Preface. Theor. Comput. Sci. 294(3): 333 (2003)

Max I. Kanovich, Mitsuhiro Okada, Andre Scedrov: Phase semantics for light linear logic. Theor. Comput. Sci. 294(3): 525-549 (2003)

Misao Nagayama, Mitsuhiro Okada: A graph-theoretic characterization theorem for multiplicative fragment of non-commutative linear logic. Theor. Comput. Sci. 294(3): 551-573 (2003)

Koji Hasebe, Mitsuhiro Okada: Inferences on Honesty in Compositional Logic for Protocol Analysis. ISSS 2003: 65-86

Mitsuhiro Okada, Benjamin C. Pierce, Andre Scedrov, Hideyuki Tokuda, Akinori Yonezawa (Eds.): Software Security -- Theories and Systems, Mext-NSF-JSPS International Symposium, ISSS 2002, Tokyo, Japan, November 8-10, 2002, Revised Papers. Lecture Notes in Computer Science 2609, Springer 2003, isbn 3-540-00708-3

Mariangiola Dezani-Ciancaglini, Mitsuhiro Okada, Masako Takahashi: Theories of Types and Proofs 1997 - Preface. Theor. Comput. Sci. 272(1-2): 1-2 (2002)

Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada: Inductive-data-type systems. Theor. Comput. Sci. 272(1-2): 41-68 (2002)

Mitsuhiro Okada: A uniform semantic proof for cut-elimination and completeness of various first and higher order logics. Theor. Comput. Sci. 281(1-2): 471-498 (2002)

Mitsuhiro Okada: Ideal Concepts, Intuitions, and Mathematical Knowledge Acquisitions in Husserl and Hilbert. Progress in Discovery Science 2002: 40-77

Koji Hasebe, Mitsuhiro Okada: A Logical Verification Method for Security Protocols Based on Linear Logic and BAN Logic. ISSS 2002: 417-440

Misao Nagayama, Mitsuhiro Okada: A New Correctness Criterion for The Proof Nets of Non-Commutative Multiplicative Linear Logics. J. Symb. Log. 66(4): 1524-1542 (2001)

Mitsuhiro Okada, Kazushige Terui: The Finite Model Property for Various Fragments of Intuitionistic Linear Logic. J. Symb. Log. 64(2): 790-802 (1999)

Mitsuhiro Okada: Phase Semantic Cut-Elimination and Normalization Proofs of First- and Higher-Order Linear Logic. Theor. Comput. Sci. 227(1-2): 333-396 (1999)

Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada: The Calculus of algebraic Constructions. RTA 1999: 301-316

Masahiro Hamano, Mitsuhiro Okada: A direct independence proof of Buchholz's Hydra Game on finite labeled trees. Arch. Math. Log. 37(2): 67-89 (1998)

Max I. Kanovich, Mitsuhiro Okada, Andre Scedrov: Specifying Real-Time Finite-State Systems in Linear Logic. Electr. Notes Theor. Comput. Sci. 16(1): 42-59 (1998)

Max I. Kanovich, Mitsuhiro Okada, Andre Scedrov: Phase semantics for light linear logic. Electr. Notes Theor. Comput. Sci. 6: 221-234 (1997)

Masahiro Hamano, Mitsuhiro Okada: A Relationship Among Gentzen's Proof-Reduction, Kirby-Paris' Hydra Game and Buchholz's Hydra Game. Math. Log. Q. 43: 103-120 (1997)

Jean-Pierre Jouannaud, Mitsuhiro Okada: Abstract Data Type Systems. Theor. Comput. Sci. 173(2): 349-391 (1997)

Jean-Yves Girard, Mitsuhiro Okada, Andre Scedrov: Preface. Electr. Notes Theor. Comput. Sci. 3: 1 (1996)

Misao Nagayama, Mitsuhiro Okada: A Graph-Theoretic Characterization Theorem for Multiplicative Fragment of Non-Commutative Linear Logic. Electr. Notes Theor. Comput. Sci. 3: 153 (1996)

Mitsuhiro Okada: Phase Semantics for Higher Order Completeness, Cut-Elimination and Normalization Proofs. Electr. Notes Theor. Comput. Sci. 3: 154 (1996)

Yexuan Gui, Mitsuhiro Okada: System Description of LAMBDALG - A Higher Order Algebraic Specification Language. LPAR 1993: 354-356

Yexuan Gui, Mitsuhiro Okada: LAMBDALG: Higher Order Algebraic Specification Language. RTA 1993: 462-466

Jean-Pierre Jouannaud, Mitsuhiro Okada: Satisfiability of Systems of Ordinal Notations with the Subterm Property is Decidable. ICALP 1991: 455-468

Jean-Pierre Jouannaud, Mitsuhiro Okada: A Computation Model for Executable Higher-Order Algebraic Specification Languages. LICS 1991: 350-361

Stéphane Kaplan, Mitsuhiro Okada (Eds.): Conditional and Typed Rewriting Systems, 2nd International CTRS Workshop, Montreal, Canada, June 11-14, 1990, Proceedings. Lecture Notes in Computer Science 516, Springer 1991, isbn 3-540-54317-1

Nachum Dershowitz, Mitsuhiro Okada: A Rationale for Conditional Equational Programming. Theor. Comput. Sci. 75(1&2): 111-138 (1990)

Mitsuhiro Okada: Strong Normalizability for the Combined System of the Typed lambda Calculus and an Arbitrary Convergent Term Rewrite System. ISSAC 1989: 357-363

Mitsuhiro Okada: On a Theory of Weak Implications. J. Symb. Log. 53(1): 200-211 (1988)

Nachum Dershowitz, Mitsuhiro Okada, G. Sivakumar: Canonical Conditional Rewrite Systems. CADE 1988: 538-549

Nachum Dershowitz, Mitsuhiro Okada: Conditional Equational Programming and the Theory of Conditional Term Rewriting. FGCS 1988: 337-346

Nachum Dershowitz, Mitsuhiro Okada: Proof-Theoretic Techniques for Term Rewriting Theory. LICS 1988: 104-111

Mitsuhiro Okada: A Simple Relationship between Buchholz's New System of Ordinal Notations and Takeuti's System of Ordinal Diagrams. J. Symb. Log. 52(3): 577-581 (1987)

Nachum Dershowitz, Mitsuhiro Okada, G. Sivakumar: Confluence of Conditional Rewrite Systems. CTRS 1987: 31-44

Mitsuhiro Okada: A Logical Analysis on Theory of Conditional Rewriting. CTRS 1987: 179-196