@article(BJO2002,
 author       = {Fr\'{e}d\'{e}ric Blanqui and Jean-Pierre Jouannaud and Mitsuhiro Okada},
 year         = {2002},
 title        = {Inductive-data-type systems},
 journal      = {Theoretical Computer Science},
 volume       = {272},
 number       = {1},
 pages        = {41--68},
 doi          = {10.1016/S0304-3975(00)00347-9},
)
@article(BJO2018,
 author       = {Fr\'{e}d\'{e}ric Blanqui and Jean-Pierre Jouannaud and Mitsuhiro Okada},
 year         = {2018},
 title        = {Corrigendum to “Inductive-data-type systems” [Theoret. Comput. Sci. 272 (1–2) (2002) 41–68]},
 journal      = {Theoretical Computer Science},
 doi          = {10.1016/j.tcs.2018.01.010},
)
@article(buchholz1987,
 author       = {Wilfried Buchholz},
 year         = {1987},
 title        = {An independence result for ($\Pi^1_1$-$CA$)$+BI$},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {33},
 pages        = {131--155},
 doi          = {10.1016/0168-0072(87)90078-9},
)
@article(dershowitz1987,
 author       = {Nachum Dershowitz},
 year         = {1987},
 title        = {Termination of rewriting},
 journal      = {Journal of Symbolic Computation},
 volume       = {3},
 number       = {1},
 pages        = {69--115},
 doi          = {10.1016/S0747-7171(87)80022-6},
)
@incollection(DJ1990,
 author       = {Nachum Dershowitz and Jean-Pierre Jouannaud},
 year         = {1990},
 title        = {Rewrite Systems},
 editor       = {Jan van Leeuwen},
 booktitle    = {Handbook of Theoretical Computer Science (Vol. B)},
 publisher    = {MIT Press},
 address      = {Cambridge, MA, USA},
 pages        = {243--320},
)
@article(DT2003,
 author       = {Nachum Dershowitz and Iddo Tzameret},
 year         = {2003},
 title        = {Gap Embedding for Well-Quasi-Orderings.},
 journal      = {Electronic Notes in Theoretical Computer Science},
 volume       = {84},
 pages        = {80--90},
 doi          = {10.1016/S1571-0661(04)80846-6},
)
@article(HO1998,
 author       = {Masahiro Hamano and Mitsuhiro Okada},
 year         = {1998},
 title        = {A direct independence proof of Buchholz's Hydra Game on finite labeled trees},
 journal      = {Archive for Mathematical Logic},
 volume       = {37},
 number       = {2},
 pages        = {67--89},
 doi          = {10.1007/s001530050084},
)
@inproceedings(isihara2007,
 author       = {Ariya Isihara},
 year         = {2007},
 title        = {Hydra Games and Tree Ordinals},
 editor       = {Daniel Leivant and Ruy de Queiroz},
 booktitle    = {Logic, Language, Information and Computation},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {238--247},
 doi          = {10.1007/978-3-540-73445-1_17},
)
@inproceedings(JO1991,
 author       = {J. P. Jouannaud and M. Okada},
 year         = {1991},
 title        = {A computation model for executable higher-order algebraic specification languages},
 booktitle    = {[1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science},
 pages        = {350--361},
 doi          = {10.1109/LICS.1991.151659},
)
@article(okada1987,
 author       = {Mitsuhiro Okada},
 year         = {1987},
 title        = {A Simple Relationship between Buchholz's New System of Ordinal Notations and Takeuti's System of Ordinal Diagrams},
 journal      = {The Journal of Symbolic Logic},
 volume       = {52},
 number       = {3},
 pages        = {577--581},
 doi          = {10.2969/jmsj/01340346},
)
@article(okada1988,
 author       = {Mitsuhiro Okada},
 year         = {1988},
 title        = {Note on a Proof of the Extended Kirby-Paris Theorem on Labeled Finite Trees},
 journal      = {European Journal of Combinatorics},
 volume       = {9},
 number       = {3},
 pages        = {249--253},
 doi          = {10.1016/S0195-6698(88)80016-7},
)
@incollection(OT1987,
 author       = {Mitsuhiro Okada and Gaisi Takeuti},
 year         = {1987},
 title        = {On the theory of quasi-ordinal diagrams},
 booktitle    = {Logic and combinatorics ({A}rcata, {C}alif., 1985)},
 series       = {Contemp. Math.},
 volume       = {65},
 publisher    = {Amer. Math. Soc., Providence, RI},
 pages        = {295--308},
 doi          = {10.1090/conm/065/891255},
)
@book(takeuti1987,
 author       = {Gaisi Takeuti},
 year         = {1987},
 title        = {Proof Theory},
 edition      = {second},
 series       = {Studies in Logic and the Foundations of Mathematics},
 volume       = {81},
 publisher    = {North-Holland},
 address      = {Amsterdam},
)