Books
1. Yoshiki Kinoshita and Makoto Takeyama, Assurance Case as a Proof in a Theory: towards Formulation of Rebuttals, in "Assuring the
Safety of Systems, Proceedings of the Twenty-first Safety-Critical Systems Symposium, Bristol, UK, 2013.
2. Keishi Okamoto, Yoshiki Kinoshita, Takahiro Seino, Noriaki Izumi, Koichi ashida and Hiroki Takamura, A design for an assessment
procedure for dependability based on a formal model, in "Proceedings of The Second IASTED International Conference on Advances in
Management Science and Risk Assessment (AMSRA2010)", 2010.
3. Yoshiki Kinoshita, Bengt Nordström, and Makoto Takeyama, A simple type-theoretic language: Mini-TT, Thierry Coquand, in “From
Semantics to Computer Science,” Y. Bertot, G. Huet, J.-J. Lévy and G. Plotkin (eds.), ISBN978-0-521-51825-3, pp.139-164, Cambridge
University Press, 2009.
4. Yutaka Matsuno, Yoshiki Kinoshita, Hiroki Takamura and Makoto, TakeyamaToward User Oriented Dependability Standard for Future
Embedded Systems, in "Proceeding, STFSSD '09 Proceedings of the 2009 Software Technologies for Future Dependable Distributed
Systems IEEE Computer Society Washington, DC, USA", Lecture Notes in Computer Science, 2009
Papers (refereed)
1. Yoshiki Kinoshita and A.J.Power, Category theoretic structure of setoids, Theoretical Computer Science, Elsevier, vol. 546, No. 21,
pp. 145–163, 2014.
2. Makoto Takeyama, Hiroyuki Kido and Yoshiki Kinoshita, Using a Proof Assistant to Construct Assurance Cases Correctness by
Construction (Fast Abstract), to appear in the Proceedings of The 42nd Annual IEEE/IFIP International Conference on Dependable
Systems and Networks (DSN 2012), 2012.
3. 木下佳樹, 帰納と再帰ー表示的意味論の第一歩, 『コンピュータソフトウェア』（岩波書店）, Vol. 29, No.1, pp.30-46, 2012.
4. Jun Kohjina, Toshimitsu Ushio and Yoshiki Kinoshita, A Coalgebraic Approach to Supervisory Control of Partially Observed Mealy
Automata, Algebra and Coalgebra in Computer Science - 4th International Conference, CALCO 2011, Winchester, UK, August 30 -
September 2, 2011. Proceedings (Springer-Verlag)6859, pp.253-267, 2011.
5. 木下佳樹、高井利憲, 記述の科学 第3回 記述の構成と利用,情報処理, 第51巻, 第10号, pp.1332-1340, 2010.
6. 木下佳樹、高井利憲, 記述の科学 第2回 視点と形式的体系,情報処理, 第51巻, 第9号, pp.1204-1214, 2010.
7. 木下佳樹、高井利憲, 記述の科学 第1回 記述とは,情報処理, 第51巻, 第8号, pp.1049-1057, 2010.
8. 木下佳樹、高井利憲, 臨床情報学のための野外科学的方法ー技術移転の方法論に向けて, 『シンセシオロジー』（産業技術総合研究所）Vol.3,
No.1, pp.36-46, 2010.
9. Yoshiki Kinoshita and Toshinori Takai, A field-scientific approach to Clinico-Informatics, Synthesiology―English Edition, Vol. 3, No. 1,
pp. 64―76, 2010.
10. Hiroyuki Ozaki, Makoto Takeyama and Yoshiki Kinoshita, Agate―an Agda-to-Haskell compiler, Computer Software (Iwanami shoten)
Vol. 26, No. 4, pp. 107-119, 2009.
11. Koki Nishizawa and Yoshiki Kinoshita, An algebraic semantics of predicate abstraction for PML, Computer Software (Iwanami shoten)
Vol.26, No.2, pp.147-156, 2009.
12. Hitoshi Furusawa and Yoshiki Kinoshita, Essentially algebraic structure for Kleene algebra with tests and its application to semantics of
while programs, IPSJ Transactions on Programming (Information Processing Society of Japan)44(SIG 4(PRO 17)), pp.47-53, 2003.
13. 古澤仁、木下佳樹, テスト付クリーニ代数の準代数構造, 『コンピュータソフトウェア』（岩波書店）20(2), pp.47-53, 2003.
14. Yoshiki Kinoshita and John A. Power, Data Refinement and algebraic structure, Acta Informatica (Springer-Verlag)36(9 and 10),
pp.693-719, 2000.
15. Yoshiki Kinoshita and John A.power, A general completeness result in refinement, in "Recent Trends in Algebraic Development
Techniques" (eds. Didier Bert, Christine Choppy and Peter D. Mosses) (Springer-Verlag)1827, pp.201-218, 2000.
16. Yoshiki Kinoshita, John A. Power and Makoto Takeyama, Sketches, Journal of Pure and Applied Algebra (Elsevier)143, pp.275-291,
1999.
17. Yoshiki Kinoshita and Koichi Takahashi, Proving Through Commutative Diagrams, in "Logic, Language and Computation,
volume 2" (eds. Lawrence S. Moss, Jonathan Ginzburg, and Maarten de Rijke), CSLI Lecture Notes (University of Chicago Press)96,
pp.128-142,1999.
18. 木下佳樹, クヌース・ベンディクスの代わりに米田ーモノイドの場合, 『コンピュータソフトウェア』（岩波書店）16(2), pp.72-75, 1998.
19. Yoshiki Kinoshita, A bicategorical analysis of E-categories, Mathematica Japonicae (International Society for Mathematical Sciences)
47(1), pp.157-169, 1998.
20. Yoshiki Kinoshita, Peter W.O'Hearn, John A.Power, Makoto Takeyama and Robert D.Tennent, An axiomatic approach to binary logical
relations with applications to data refinement, Lecture Notes in Computer Science (Springer-Verlag)1281, pp.191-212, 1997.
21. 木下佳樹、高橋功一、中田秀基, 証明支援系の図式によるインターフェイス, 『コンピュータソフトウェア』（岩波書店）14(3), pp.42-50, 1997.
22. Yoshiki Kinoshita and A. John Power, Lax naturality through enrichment, Journal of Pure and Applied Algebra (Elsevier)112(1),
pp.53-72, 1996.
23. Yoshiki Kinoshita and A. John Power, Data Refinement for Call-By-Value Programming Lanuages, Lecture Notes in Computer Science
(Springer-Verlag) 1683, pp.562-576, 1996.
24. Yoshiki Kinoshita and John A.Power, A fibrational semantics of logic programs, in "Extensions of Logic Programming, 5th International
Workshop, ELP'96, Leipzig, Germany", Extensions of Logic Programming, 5th International Workshop, ELP'96, Leipzig, Germany
(Springer-Verlag)1050, pp.177-192, 1996.
Papers (not refereed)
1. 木下佳樹, 武山誠, 平井誠, 湯浅能史, ファイル共有サービスの形式アシュランスケース－事例研究－, Science Journal of Kanagawa
University, Vol.25, pp.39-50, 2014.
2. 木下佳樹, 森口草介,中原早生, 組込みシステムデモンストレーションの効果に関するアシュランスケース事例, Science Journal of Kanagawa
University, Vol.25, pp.51-56, 2014.
3. 木下佳樹、高井利憲、大崎人士, フォーマルメソッドのフィールドワーク, 『情報処理』（情報処理学会）, 49(5),pp.499-505, 2008.
4. Satoshi Matsuoka, Yoshiki KInoshita, Koichi Takahashi, Mitsuru Tanaka, Takeshi Ito and Tsuyoshi Hamakawa, Improvement on Integrity
Checking System for Software in Weighing Instrument, (Electronic publishing), 2005.
Others
1. Yoshiki Kinoshita, Standardization in Open systems dependability, in “Open Systems Dependability: Dependability Engineering for
Ever-Changing Systems”, Second Edition, Mario Tokoro (ed.), ISBN-13: 978-1498736282, pp.229-243, CRC Press, 2015.
2. 木下佳樹, 妥当性確認とアシュランスケース(独)科学技術振興機構 研究開発戦略センター システム科学ユニット 第8回システム科学検討会,
2014.
3. 和泉憲明、岡本圭史、木下佳樹、高井利憲、高村博紀、田口研治、武山誠、水口大知, オープンシステムディペンダビリティと利用者指向～
課題と解決へのアプローチ～, 『第8回ディペンダブルシステムワークショップ予稿集』日本ソフトウェア科学会, 2010.
4. 木下佳樹, User Oriented Dependability, 『第7回ディペンダブルシステムワークショップ予稿集』日本ソフトウェア科学会, 2009.
5. 中野哲、今井林太郎、樋口崇、木下佳樹、岡本圭史、武山誠、安部達也、齋藤正也, Formalization of System LSI Specification and Automatic
Generation of Verification Items, 『算譜科学研究速報』（産業技術総合研究所）PS-2009-006, 2009.
6. Yoshiki Kinoshita, Fieldwork and the 4:6 Principle-Introduction to the Research Center for Verification and Semantics, in "Proceedings of
IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing, 2009. ISORC '09", IEEE
Computer Society, 2009.
7. 木下佳樹, Agda言語について, 『日本ソフトウェア科学会第25回大会予稿集』（日本ソフトウェア科学会）, 2008.
8. 青木利晃、粂野文洋、木下佳樹、篠崎孝一、高野理、高村博紀、田口研治、中原早生、西原秀明、早水公二、本位田真一、渡邊宏、モデル検査の
教育プログラム構築に向けて, 算譜科学研究速報（産業技術総合研究所）PS-2008-012, 2008.
9. 木下佳樹, 書類の定式化と検証, 第6回ディペンダブルシステムワークショップ予稿集（日本ソフトウェア科学会）, 2008.
10. 木下佳樹、高村博紀, 型理論での形式的証明記述の技法について, 日本ソフトウェア科学会第22回大会予稿集, 2005.
11. Hiroshi Watanabe and Yoshiki Kinoshita, A Functorial Approach to Refinement, AIST Programing Science Group Technical ReportAIST-
PS-2001-01, pp.49-63, 2001.
12. 木下佳樹, "ソフトウェアの複雑さ, 『Computer Today』（サイエンス社）, Vol.15, No.3, pp.18-23, 1998.
13. Koichi Takahashi and Yoshiki Kinoshita, Groupoid of Equational Proofs, 『電子技術総合研究所彙報』（オーム社）, Vol.60, No.1,
pp.711-718, 1996.
14. 木下佳樹, ソフトウェアの差分, 「協調プログラミング例題集「文殊の知恵」を目指して」、bit別冊、共立出版, pp.59-60, 1996.