| 2008 |
|---|
| 45 | EE | Koji Mineshima,
Mitsuhiro Okada,
Yuri Sato,
Ryo Takemura:
Diagrammatic Reasoning System with Euler Circles: Theory and Experiment Design.
Diagrams 2008: 188-205 |
| 2007 |
|---|
| 44 | EE | Gergei Bana,
Koji Hasebe,
Mitsuhiro Okada:
Computational Semantics for Basic Protocol Logic - A Stochastic Approach.
ASIAN 2007: 86-94 |
| 43 | EE | 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 |
| 2006 |
|---|
| 42 | EE | 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 |
| 41 | EE | Frédéric Blanqui,
Jean-Pierre Jouannaud,
Mitsuhiro Okada:
The Calculus of Algebraic Constructions
CoRR abs/cs/0610063: (2006) |
| 40 | EE | Frédéric Blanqui,
Jean-Pierre Jouannaud,
Mitsuhiro Okada:
Inductive-data-type Systems
CoRR abs/cs/0610066: (2006) |
| 39 | EE | 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) |
| 38 | EE | Max I. Kanovich,
Mitsuhiro Okada,
Kazushige Terui:
Intuitionistic phase semantics is almost classical.
Mathematical Structures in Computer Science 16(1): 67-86 (2006) |
| 2003 |
|---|
| 37 | | Mitsuhiro Okada,
Benjamin C. Pierce,
Andre Scedrov,
Hideyuki Tokuda,
Akinori Yonezawa:
Software Security -- Theories and Systems, Mext-NSF-JSPS International Symposium, ISSS 2002, Tokyo, Japan, November 8-10, 2002, Revised Papers
Springer 2003 |
| 36 | EE | Koji Hasebe,
Mitsuhiro Okada:
Inferences on Honesty in Compositional Logic for Protocol Analysis.
ISSS 2003: 65-86 |
| 35 | | Jean-Yves Girard,
Mitsuhiro Okada,
Andre Scedrov:
Preface.
Theor. Comput. Sci. 294(3): 333 (2003) |
| 34 | | Max I. Kanovich,
Mitsuhiro Okada,
Andre Scedrov:
Phase semantics for light linear logic.
Theor. Comput. Sci. 294(3): 525-549 (2003) |
| 33 | | 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) |
| 2002 |
|---|
| 32 | EE | Koji Hasebe,
Mitsuhiro Okada:
A Logical Verification Method for Security Protocols Based on Linear Logic and BAN Logic.
ISSS 2002: 417-440 |
| 31 | EE | Koji Hasebe,
Mitsuhiro Okada:
Formal Analysis of the iKP Electronic Payment Protocols.
ISSS 2002: 441-460 |
| 30 | EE | Mitsuhiro Okada:
Ideal Concepts, Intuitions, and Mathematical Knowledge Acquisitions in Husserl and Hilbert.
Progress in Discovery Science 2002: 40-77 |
| 29 | EE | Mariangiola Dezani-Ciancaglini,
Mitsuhiro Okada,
Masako Takahashi:
Theories of Types and Proofs 1997 - Preface.
Theor. Comput. Sci. 272(1-2): 1-2 (2002) |
| 28 | EE | Frédéric Blanqui,
Jean-Pierre Jouannaud,
Mitsuhiro Okada:
Inductive-data-type systems.
Theor. Comput. Sci. 272(1-2): 41-68 (2002) |
| 27 | EE | 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) |
| 2001 |
|---|
| 26 | | 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) |
| 1999 |
|---|
| 25 | EE | Frédéric Blanqui,
Jean-Pierre Jouannaud,
Mitsuhiro Okada:
The Calculus of algebraic Constructions.
RTA 1999: 301-316 |
| 24 | | Mitsuhiro Okada,
Kazushige Terui:
The Finite Model Property for Various Fragments of Intuitionistic Linear Logic.
J. Symb. Log. 64(2): 790-802 (1999) |
| 23 | EE | 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) |
| 1998 |
|---|
| 22 | EE | 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) |
| 21 | EE | Max I. Kanovich,
Mitsuhiro Okada,
Andre Scedrov:
Specifying Real-Time Finite-State Systems in Linear Logic.
Electr. Notes Theor. Comput. Sci. 16(1): (1998) |
| 1997 |
|---|
| 20 | EE | Max I. Kanovich,
Mitsuhiro Okada,
Andre Scedrov:
Phase semantics for light linear logic.
Electr. Notes Theor. Comput. Sci. 6: (1997) |
| 19 | | 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) |
| 18 | EE | Jean-Pierre Jouannaud,
Mitsuhiro Okada:
Abstract Data Type Systems.
Theor. Comput. Sci. 173(2): 349-391 (1997) |
| 1996 |
|---|
| 17 | EE | Misao Nagayama,
Mitsuhiro Okada:
A Graph-Theoretic Characterization Theorem for Multiplicative Fragment of Non-Commutative Linear Logic.
Electr. Notes Theor. Comput. Sci. 3: (1996) |
| 16 | EE | Mitsuhiro Okada:
Phase Semantics for Higher Order Completeness, Cut-Elimination and Normalization Proofs.
Electr. Notes Theor. Comput. Sci. 3: (1996) |
| 15 | EE | Jean-Yves Girard,
Mitsuhiro Okada,
Andre Scedrov:
Preface.
Electr. Notes Theor. Comput. Sci. 3: (1996) |
| 1993 |
|---|
| 14 | | Yexuan Gui,
Mitsuhiro Okada:
System Description of LAMBDALG - A Higher Order Algebraic Specification Language.
LPAR 1993: 354-356 |
| 13 | | Yexuan Gui,
Mitsuhiro Okada:
LAMBDALG: Higher Order Algebraic Specification Language.
RTA 1993: 462-466 |
| 1991 |
|---|
| 12 | | Stéphane Kaplan,
Mitsuhiro Okada:
Conditional and Typed Rewriting Systems, 2nd International CTRS Workshop, Montreal, Canada, June 11-14, 1990, Proceedings
Springer 1991 |
| 11 | | Jean-Pierre Jouannaud,
Mitsuhiro Okada:
Satisfiability of Systems of Ordinal Notations with the Subterm Property is Decidable.
ICALP 1991: 455-468 |
| 10 | | Jean-Pierre Jouannaud,
Mitsuhiro Okada:
A Computation Model for Executable Higher-Order Algebraic Specification Languages
LICS 1991: 350-361 |
| 1990 |
|---|
| 9 | | Nachum Dershowitz,
Mitsuhiro Okada:
A Rationale for Conditional Equational Programming.
Theor. Comput. Sci. 75(1&2): 111-138 (1990) |
| 1989 |
|---|
| 8 | EE | Mitsuhiro Okada:
Strong Normalizability for the Combined System of the Typed lambda Calculus and an Arbitrary Convergent Term Rewrite System.
ISSAC 1989: 357-363 |
| 1988 |
|---|
| 7 | | Nachum Dershowitz,
Mitsuhiro Okada,
G. Sivakumar:
Canonical Conditional Rewrite Systems.
CADE 1988: 538-549 |
| 6 | | Nachum Dershowitz,
Mitsuhiro Okada:
Conditional Equational Programming and the Theory of Conditional Term Rewriting.
FGCS 1988: 337-346 |
| 5 | | Nachum Dershowitz,
Mitsuhiro Okada:
Proof-Theoretic Techniques for Term Rewriting Theory
LICS 1988: 104-111 |
| 4 | | Mitsuhiro Okada:
On a Theory of Weak Implications.
J. Symb. Log. 53(1): 200-211 (1988) |
| 1987 |
|---|
| 3 | | Mitsuhiro Okada:
A Logical Analysis on Theory of Conditional Rewriting.
CTRS 1987: 179-196 |
| 2 | | Nachum Dershowitz,
Mitsuhiro Okada,
G. Sivakumar:
Confluence of Conditional Rewrite Systems.
CTRS 1987: 31-44 |
| 1 | | 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) |
